#6523 and other heap-use-after-free error

Z3Prover · Nov 7, 2023 · e86eae2 · e86eae2
1 parent eed02b6
commit e86eae2
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 11 deletions.
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
@@ -1042,7 +1042,10 @@ namespace arith {
         SASSERT(m_nla);
         SASSERT(m_nla->use_nra_model());
         auto t = get_tv(v);
-        if (t.is_term()) {
+        if (!t.is_term()) {
+            m_nla->am().set(r, m_nla->am_value(t.id()));
+        }
+        else {
             m_todo_terms.push_back(std::make_pair(t, rational::one()));
             TRACE("nl_value", tout << "v" << v << " " << t.to_string() << "\n";);
             TRACE("nl_value", tout << "v" << v << " := w" << t.to_string() << "\n";
@@ -1072,11 +1075,8 @@ namespace arith {
                     }
                 }
             }
-            return r;
-        }
-        else {
-            return m_nla->am_value(t.id());
         }
+        return r;
     }
 
     lbool solver::make_feasible() {

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -1954,7 +1954,7 @@ class theory_lra::imp {
             }
             // The call mk_bound() can set the m_infeasible_column in lar_solver
             // so the explanation is safer to take before this call.
-            app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
+            expr_ref b(mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper()), m);
             if (m.has_trace_stream()) {
                 th.log_axiom_instantiation(b);
                 m.trace_stream() << "[end-of-instance]\n";
@@ -3381,7 +3381,9 @@ class theory_lra::imp {
     nlsat::anum const& nl_value(theory_var v, scoped_anum& r) const {
         SASSERT(use_nra_model());
         auto t = get_tv(v);
-        if (t.is_term()) {
+        if (!t.is_term())
+            m_nla->am().set(r, m_nla->am_value(t.id()));            
+        else {
 
             m_todo_terms.push_back(std::make_pair(t, rational::one()));
             TRACE("nl_value", tout << "v" << v << " " << t.to_string() << "\n";);
@@ -3412,11 +3414,9 @@ class theory_lra::imp {
                     }
                 }
             }
-            return r;
-        }
-        else {
-            return m_nla->am_value(t.id());
         }
+        return r;
+
     }
 
     model_value_proc * mk_value(enode * n, model_generator & mg) {