diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg
index 1a043b6fbc..ba537890a5 100644
--- a/src/params/smt_parallel_params.pyg
+++ b/src/params/smt_parallel_params.pyg
@@ -3,6 +3,7 @@ def_module_params('smt_parallel',
                   description='Experimental parameters for parallel solving',
                   params=(
                         ('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'),
+                        ('force_enable', BOOL, False, 'force the SMT parallel architecture even when smt.threads is 1'),
                         ('sls', BOOL, False, 'add sls-tactic as a separate worker thread outside the search tree parallelism'),
 	                  ('num_global_bb_fl_threads', UINT, 0, 'run failed-literal backbone worker threads; default is 0 (off), supported values are 1 (negative mode only) or 2 (negative and positive mode)'),
                         ('num_global_bb_batch_threads', UINT, 0, 'run Janota-style chunking backbone worker threads; default is 0 (off), supported values are 1 (negative mode only) or 2 (negative and positive mode)'),
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 7b0a8d5ee7..89326fa7ac 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -32,6 +32,7 @@ Revision History:
 #include "model/model_params.hpp"
 #include "model/model.h"
 #include "model/model_pp.h"
+#include "params/smt_parallel_params.hpp"
 #include "smt/smt_context.h"
 #include "smt/smt_quick_checker.h"
 #include "smt/uses_theory.h"
@@ -3615,6 +3616,13 @@ namespace smt {
         return m_model.get() != nullptr;
     }
 
+    bool context::use_parallel_solver() const {
+        if (m.has_trace_stream() || m_par)
+            return false;
+        smt_parallel_params pp(m_params);
+        return m_fparams.m_threads > 1 || pp.force_enable();
+    }
+
     /**
        \brief Setup the logical context based on the current set of
        asserted formulas and execute the check command.
@@ -3628,7 +3636,7 @@ namespace smt {
         SASSERT(!m_setup.already_configured());
         setup_context(m_fparams.m_auto_config);
 
-        if (m_fparams.m_threads > 1 && !m.has_trace_stream()) {
+        if (use_parallel_solver()) {
             parallel p(*this);
             expr_ref_vector asms(m);
             return p(asms);
@@ -3695,7 +3703,7 @@ namespace smt {
         SASSERT(at_base_level());
         setup_context(false);
         search_completion sc(*this);
-        if (m_fparams.m_threads > 1 && !m.has_trace_stream()) {            
+        if (use_parallel_solver()) {            
             expr_ref_vector asms(m, num_assumptions, assumptions);
             parallel p(*this);
             return p(asms);
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 02da5d15fe..4f7774b087 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -131,6 +131,7 @@ namespace smt {
         bool                        m_is_auxiliary = false; // used to prevent unwanted information from being logged.
         class parallel*             m_par = nullptr;
         unsigned                    m_par_index = 0;
+        bool                        use_parallel_solver() const;
         bool                        m_internalizing_assertions = false;
         lbool                       m_internal_completed = l_undef;
 
@@ -1918,4 +1919,3 @@ namespace smt {
 
 };
 
-
diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 7d6dbe6120..6b965c5e48 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -854,6 +854,7 @@ namespace smt {
         LOG_WORKER(1, " created with " << asms.size() << " assumptions\n");
         m_smt_params.m_random_seed += id;  // ensure different random seed for each worker
         ctx = alloc(context, m, m_smt_params, p.ctx.get_params());
+        ctx->m_par = &p;
         ctx->set_logic(p.ctx.m_setup.get_logic());
         context::copy(p.ctx, *ctx, true);
         // don't share initial units
@@ -1839,7 +1840,9 @@ namespace smt {
         m_core_minimizer_worker = nullptr;
         scoped_limits sl(m.limit());
         flet<unsigned> _nt(ctx.m_fparams.m_threads, 1);
-        SASSERT(num_workers > 1);
+        if (num_workers == 0)
+            throw default_exception("smt.threads must be at least 1 in parallel mode");
+        SASSERT(num_workers > 1 || pp.force_enable());
         for (unsigned i = 0; i < num_workers; ++i)
             m_workers.push_back(alloc(worker, i, *this, asms));
         for (auto w : m_workers)