diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 309b08297..a86499149 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1505,6 +1505,9 @@ class PythonInstallComponent(Component):
                                            os.path.join(self.pythonPkgDir, 'z3', '__pycache__', '*.pyc'),
                                            in_prefix=self.in_prefix_install
                                           )
+        MakeRuleCmd.remove_installed_files(out,
+                                           os.path.join(self.pythonPkgDir, 'z3', 'lib',
+                                                        self.libz3Component.dll_file()))
 
     def mk_makefile(self, out):
         return
diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index 4f538867e..8871c3dd8 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -224,12 +224,12 @@ struct pb2bv_rewriter::imp {
     public:
 
         card2bv_rewriter(imp& i, ast_manager& m):
+            m_sort(*this),
             m(m),
             m_imp(i),
             au(m),
             pb(m),
             bv(m),
-            m_sort(*this),
             m_trail(m),
             m_args(m)
         {}
diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp
index 79495e24f..a73f7ed38 100644
--- a/src/test/qe_arith.cpp
+++ b/src/test/qe_arith.cpp
@@ -375,6 +375,9 @@ static void add_random_ineq(
     case opt::t_le:
         fml = a.mk_le(t1, t2);
         break;
+    case opt::t_mod:
+        NOT_IMPLEMENTED_YET();        
+        break;        
     }
     fmls.push_back(fml);
     mbo.add_constraint(vars, rational(coeff), rel);