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;
 
         //
diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h
index b337d5e45..838e2f84c 100644
--- a/src/smt/smt_parallel.h
+++ b/src/smt/smt_parallel.h
@@ -96,8 +96,8 @@ namespace smt {
             expr_ref_vector asms;
             smt_params m_smt_params;
             scoped_ptr<context> ctx;
-            unsigned m_max_conflicts = 800; // the global budget for all work this worker can do across cubes in the current run.
-            unsigned m_max_thread_conflicts = 100; // the per-cube limit for how many conflicts the worker can spend on a single cube before timing out on it and moving on
+            unsigned m_max_conflicts; // the global budget for all work this worker can do across cubes in the current run. THIS GETS SET IN THE CPP FILE
+            unsigned m_max_thread_conflicts; // the per-cube limit for how many conflicts the worker can spend on a single cube before timing out on it and moving on. THIS GETS SET IN THE CPP FILE
             unsigned m_num_shared_units = 0;
             unsigned m_shared_clause_limit = 0; // remembers the index into shared_clause_trail marking the boundary between "old" and "new" clauses to share
             void share_units(ast_translation& l2g);