fix #6580

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Feb 13, 2023 · bb81bc5 · bb81bc5
1 parent 102eee7
commit bb81bc5
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git 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
@@ -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;