diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index 8a9188e2b..4b7920596 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -31,6 +31,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_restart_strategy = static_cast<restart_strategy>(p.restart_strategy());
     m_restart_factor = p.restart_factor();
     m_case_split_strategy = static_cast<case_split_strategy>(p.case_split());
+    m_theory_case_split = p.theory_case_split();
     m_delay_units = p.delay_units();
     m_delay_units_threshold = p.delay_units_threshold();
     m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
@@ -155,4 +156,4 @@ void smt_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_check_at_labels);
     DISPLAY_PARAM(m_dump_goal_as_smt);
     DISPLAY_PARAM(m_auto_config);
-}
\ No newline at end of file
+}
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index 366570365..c03eaeaef 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -109,6 +109,7 @@ struct smt_params : public preprocessor_params,
     case_split_strategy m_case_split_strategy;
     unsigned            m_rel_case_split_order;
     bool                m_lookahead_diseq;
+    bool                m_theory_case_split;
 
     // -----------------------------------
     //
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 6ac4aab04..faa48400d 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -61,6 +61,7 @@ def_module_params(module_name='smt',
                           ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'),
                           ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
                           ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
+                          ('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.'),
                           ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
                           ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
                           ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),