diff --git a/src/sat/smt/arith_sls.cpp b/src/sat/smt/arith_sls.cpp index d7a85cdb1f8..7afabe2474e 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 c5b706fded3..d26ea516ac9 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1596,8 +1596,12 @@ class theory_lra::imp { 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;