DEFAULT_POSITIVE_ELEMENTS_SIZE
positive_params.max_elemsize = DEFAULT_POSITIVE_ELEMENTS_SIZE;
positive_params.satisf_elemsize = DEFAULT_POSITIVE_ELEMENTS_SIZE / 2;