fix #7024

Z3Prover · Nov 29, 2023 · 41a3196 · 41a3196
1 parent d469c10
commit 41a3196
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
@@ -95,7 +95,7 @@ namespace nla {
 
     scoped_anum& solver::tmp2() {
         SASSERT(use_nra_model());
-        return m_core->m_nra.tmp1();
+        return m_core->m_nra.tmp2();
     }
 
 

diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
@@ -918,7 +918,7 @@ namespace arith {
             theory_var v = (i + start) % sz;
             if (is_bool(v))
                 continue;
-            if (!ctx.is_shared(var2enode(v)) && !include_func_interp(var2enode(v)))
+            if (!ctx.is_shared(var2enode(v)))
                 continue;
             ensure_column(v);
             if (!is_registered_var(v))

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -1513,7 +1513,7 @@ class theory_lra::imp {
         for (theory_var i = 0; i < sz; ++i) {
             theory_var v = (i + start) % sz;
             enode* n1 = get_enode(v);
-            if (!th.is_relevant_and_shared(n1) && !include_func_interp(n1))                     
+            if (!th.is_relevant_and_shared(n1))                   
                 continue;
             ensure_column(v);
             if (!is_registered_var(v))