diff --git a/src/ast/simplifier/bv_simplifier_params.cpp b/src/ast/simplifier/bv_simplifier_params.cpp
index aa9dcfc2d..5d6cd363f 100644
--- a/src/ast/simplifier/bv_simplifier_params.cpp
+++ b/src/ast/simplifier/bv_simplifier_params.cpp
@@ -18,9 +18,12 @@ Revision History:
 --*/
 #include"bv_simplifier_params.h"
 #include"bv_simplifier_params_helper.hpp"
+#include"bv_rewriter_params.hpp"
 
 void bv_simplifier_params::updt_params(params_ref const & _p) {
     bv_simplifier_params_helper p(_p);
-    m_hi_div0 = p.bv_hi_div0();
+    bv_rewriter_params rp(_p);
+    m_hi_div0 = rp.hi_div0();
     m_bv2int_distribute = p.bv_bv2int_distribute();
+
 }
diff --git a/src/ast/simplifier/bv_simplifier_params_helper.pyg b/src/ast/simplifier/bv_simplifier_params_helper.pyg
index 24bc86150..6bcf83207 100644
--- a/src/ast/simplifier/bv_simplifier_params_helper.pyg
+++ b/src/ast/simplifier/bv_simplifier_params_helper.pyg
@@ -1,6 +1,4 @@
 def_module_params(class_name='bv_simplifier_params_helper',
                   module_name="old_simplify", # Parameters will be in the old_simplify module
                   export=True,
-                  params=(
-                          ('bv.hi_div0', BOOL, True, 'if true, then Z3 uses the usual hardware interpretation for division (rem, mod) by zero; otherwise, these operations are considered uninterpreted'),
-                          ('bv.bv2int_distribute', BOOL, True, 'if true, then int2bv is distributed over arithmetical operators')))
+                  params=(('bv.bv2int_distribute', BOOL, True, 'if true, then int2bv is distributed over arithmetical operators'),))