From 41a3196c890c9cff15b664679cd1cc0b951ad57f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 29 Nov 2023 13:35:30 -0800 Subject: [PATCH] fix #7024 --- src/math/lp/nla_solver.cpp | 2 +- src/sat/smt/arith_solver.cpp | 2 +- src/smt/theory_lra.cpp | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 5ed9b4538..23d4016bd 100644 --- 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 index 537291280..a32a4e964 100644 --- 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 index bbe29da74..8669a514c 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1513,7 +1513,7 @@ public: 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))