From e86eae27e644370254e9ec2a9f6b9ff5434f682a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Nov 2023 12:19:43 +0100
Subject: [PATCH] #6523 and other heap-use-after-free error

---
 src/sat/smt/arith_solver.cpp | 10 +++++-----
 src/smt/theory_lra.cpp       | 12 ++++++------
 2 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index cb2ac53ba..cefbbbf54 100644
--- 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
index 7fd31ae8c..2491d403e 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1954,7 +1954,7 @@ public:
             }
             // 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 @@ public:
     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 @@ public:
                     }
                 }
             }
-            return r;
-        }
-        else {
-            return m_nla->am_value(t.id());
         }
+        return r;
+
     }
 
     model_value_proc * mk_value(enode * n, model_generator & mg) {