From bb81bc5452f9c93a1044544b8b4d6034b22177ce Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Feb 2023 20:21:53 -0800 Subject: [PATCH] fix #6580 Signed-off-by: Nikolaj Bjorner --- src/sat/smt/arith_sls.cpp | 2 +- src/smt/theory_lra.cpp | 6 +++++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/arith_sls.cpp b/src/sat/smt/arith_sls.cpp index d7a85cdb1..7afabe247 100644 --- a/src/sat/smt/arith_sls.cpp +++ b/src/sat/smt/arith_sls.cpp @@ -62,7 +62,7 @@ namespace arith { // first compute assignment to terms // then update non-basic variables in tableau. for (auto const& [t, v] : m_terms) { - int64_t val; + int64_t val = 0; lp::lar_term const& term = s.lp().get_term(t); for (lp::lar_term::ival arg : term) { auto t2 = s.lp().column2tv(arg.column()); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index c5b706fde..d26ea516a 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1596,8 +1596,12 @@ public: final_check_status eval_power(expr* e) { expr* x, * y; + rational r; VERIFY(a.is_power(e, x, y)); - + if (a.is_numeral(x, r) && r == 0 && a.is_numeral(y, r) && r == 0) + return FC_DONE; + if (!m_nla) + return FC_GIVEUP; switch (m_nla->check_power(get_lpvar(e), get_lpvar(x), get_lpvar(y), m_nla_lemma_vector)) { case l_true: return FC_DONE;