diff --git a/src/muz_qe/qe.cpp b/src/muz_qe/qe.cpp
index 5603b8102..894a935b5 100644
--- a/src/muz_qe/qe.cpp
+++ b/src/muz_qe/qe.cpp
@@ -2084,7 +2084,7 @@ namespace qe {
             
             flet<bool> fl1(m_fparams.m_model, true);
             flet<bool> fl2(m_fparams.m_simplify_bit2int, true);
-            //flet<bool> fl3(m_fparams.m_arith_enum_const_mod, true);
+            flet<bool> fl3(m_fparams.m_arith_enum_const_mod, true);
             flet<bool> fl4(m_fparams.m_bv_enable_int2bv2int, true);
             flet<bool> fl5(m_fparams.m_array_canonize_simplify, true);
             flet<unsigned> fl6(m_fparams.m_relevancy_lvl, 0);
diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp
index dcffa83dc..7281a5daa 100644
--- a/src/smt/params/theory_arith_params.cpp
+++ b/src/smt/params/theory_arith_params.cpp
@@ -33,7 +33,6 @@ void theory_arith_params::updt_params(params_ref const & _p) {
     m_arith_int_eq_branching = p.arith_int_eq_branch();
     m_arith_ignore_int = p.arith_ignore_int();
     m_arith_bound_prop = static_cast<bound_prop_mode>(p.arith_propagation_mode());
-    m_arith_enum_const_mod = true;
 }