Merge pull request #8766 from Z3Prover/copilot/fix-critical-bugs-from-discussion

Fix critical static-analysis true positives: null deref, division by zero, dangling pointer

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);
     }

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;
         }
     };
 

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); 

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;
     }