diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index ce9c1c85c..18f6bf578 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -164,7 +164,7 @@ extern "C" {
         model::scoped_model_completion _scm(*_m, model_completion);
         result = (*_m)(to_expr(t));
         mk_c(c)->save_ast_trail(result.get());
-        *v = of_ast(result.get());
+        if (v) *v = of_ast(result.get());
         RETURN_Z3_model_eval true;
         Z3_CATCH_RETURN(false);
     }
diff --git a/src/qe/mbp/mbp_arrays.cpp b/src/qe/mbp/mbp_arrays.cpp
index 269aea213..2c3e6ddf3 100644
--- a/src/qe/mbp/mbp_arrays.cpp
+++ b/src/qe/mbp/mbp_arrays.cpp
@@ -531,6 +531,8 @@ namespace mbp {
             }
             arr_vars.shrink(j);
             aux_vars.append (m_aux_vars);
+            m_mev = nullptr;
+            M = nullptr;
         }
     };
 
diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp
index 41628372f..460a051ab 100644
--- a/src/sat/smt/pb_solver.cpp
+++ b/src/sat/smt/pb_solver.cpp
@@ -834,7 +834,7 @@ namespace pb {
     }
 
     void solver::ineq::divide(unsigned c) {
-        if (c == 1) return;
+        if (c <= 1) return;
         for (unsigned i = size(); i-- > 0; ) {
             m_wlits[i].first = (coeff(i) + c - 1) / c;
         }
@@ -857,7 +857,7 @@ namespace pb {
      */
     void solver::round_to_one(ineq& ineq, bool_var v) {
         unsigned c = ineq.bv_coeff(v);
-        if (c == 1) return;
+        if (c <= 1) return;
         unsigned sz = ineq.size();
         for (unsigned i = 0; i < sz; ++i) {
             unsigned ci = ineq.coeff(i); 
diff --git a/src/util/checked_int64.h b/src/util/checked_int64.h
index 41ac88ef7..ceae0c70c 100644
--- a/src/util/checked_int64.h
+++ b/src/util/checked_int64.h
@@ -187,11 +187,15 @@ public:
     }
 
     checked_int64& operator/=(checked_int64 const& other) {
+        if (CHECK && other.m_value == 0)
+            throw overflow_exception();
         m_value /= other.m_value;
         return *this;
     }
 
     checked_int64& operator%=(checked_int64 const& other) {
+        if (CHECK && other.m_value == 0)
+            throw overflow_exception();
         m_value %= other.m_value;
         return *this;
     }