diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 151a42d24..816764896 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -54,6 +54,8 @@ def_module_params(module_name='smt',
                           ('arith.ignore_int', BOOL, False, 'treat integer variables as real'),
                           ('arith.dump_lemmas', BOOL, False, 'dump arithmetic theory lemmas to files'),
                           ('arith.greatest_error_pivot', BOOL, False, 'Pivoting strategy'),
+                          ('arith.eager_eq_axioms', BOOL, True, 'eager equality axioms'),
+                          ('arith.auto_config_simplex', BOOL, False, 'force simplex solver in auto_config'),
                           ('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'),
                           ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'),
                           ('pb.enable_compilation', BOOL, True, 'enable compilation into sorting circuits for Pseudo-Boolean'),
diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp
index 250848db4..0918c9423 100644
--- a/src/smt/params/theory_arith_params.cpp
+++ b/src/smt/params/theory_arith_params.cpp
@@ -37,6 +37,9 @@ void theory_arith_params::updt_params(params_ref const & _p) {
     m_arith_bound_prop = static_cast<bound_prop_mode>(p.arith_propagation_mode());
     m_arith_dump_lemmas = p.arith_dump_lemmas();
     m_arith_reflect = p.arith_reflect();
+    m_arith_eager_eq_axioms = p.arith_eager_eq_axioms();
+    m_arith_auto_config_simplex = p.arith_auto_config_simplex();
+
     arith_rewriter_params ap(_p);
     m_arith_eq2ineq = ap.eq2ineq();
 }