#6971

clear m_a1, m_a2 before calls that may affect model.
Z3Prover · Nov 1, 2023 · ea915e5 · ea915e5
1 parent 3af2b36
commit ea915e5
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
@@ -1518,6 +1518,7 @@ namespace arith {
 
     void solver::propagate_nla() {
         if (m_nla) {
+            m_a1 = nullptr; m_a2 = nullptr;
             m_nla->propagate();
             add_lemmas();
             lp().collect_more_rows_for_lp_propagation();

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -2178,6 +2178,8 @@ class theory_lra::imp {
 
     void propagate_nla() {
         if (m_nla) {
+            m_a1 = nullptr; 
+            m_a2 = nullptr;
             m_nla->propagate();
             add_lemmas();
             lp().collect_more_rows_for_lp_propagation();
@@ -3385,7 +3387,7 @@ class theory_lra::imp {
     }
 
     nlsat::anum const& nl_value(theory_var v, scoped_anum& r) const {
-        SASSERT(use_nra_model());
+        SASSERT(m_nla && m_nla->use_nra_model());
         auto t = get_tv(v);
         if (t.is_term()) {