diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg index 89891deb1..cfb5f276f 100644 --- a/src/params/smt_parallel_params.pyg +++ b/src/params/smt_parallel_params.pyg @@ -5,5 +5,5 @@ def_module_params('smt_parallel', ('share_units', BOOL, True, 'share units'), ('share_conflicts', BOOL, True, 'share conflicts'), ('never_cube', BOOL, False, 'never cube'), - ('only_eager_cube', BOOL, False, 'only eager cube'), + ('frugal_cube_only', BOOL, False, 'only apply frugal cube strategy'), )) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 9bbf704d2..86f9d5a21 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -362,7 +362,7 @@ namespace smt { std::scoped_lock lock(mux); unsigned max_cubes = 1000; - bool greedy_mode = (m_cubes.size() <= max_cubes); + bool greedy_mode = (m_cubes.size() <= max_cubes) && !smt_parallel_params(p.ctx.m_params).frugal_cube_only(); unsigned a_worker_start_idx = 0; //