fixes for #6590

Z3Prover · Feb 15, 2023 · 7c08e53 · 7c08e53
1 parent c1ecc49
commit 7c08e53
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 9 deletions.
diff --git a/src/math/lp/nla_powers.cpp b/src/math/lp/nla_powers.cpp
@@ -79,6 +79,7 @@ am().set(rval, am_value(r));
 namespace nla {
 
     lbool powers::check(lpvar r, lpvar x, lpvar y, vector<lemma>& lemmas) {
+        TRACE("nla", tout << r << " == " << x << "^" << y << "\n");
         if (x == null_lpvar || y == null_lpvar || r == null_lpvar)
             return l_undef;
         if (lp::tv::is_term(x) || lp::tv::is_term(y) || lp::tv::is_term(r))
@@ -145,17 +146,24 @@ namespace nla {
             auto r2val = power(xval, yval.get_unsigned());
             if (rval == r2val)
                 return l_true;
-            if (xval > 0 && r2val < rval) {
-                SASSERT(yval > 0);
+            if (c.random() % 2 == 0) {
+                new_lemma lemma(c, "x == x0, y == y0 => r = x0^y0");
+                lemma |= ineq(x, llc::NE, xval);
+                lemma |= ineq(y, llc::NE, yval);
+                lemma |= ineq(r, llc::EQ, r2val);
+                return l_false;
+            }
+            if (yval > 0 && r2val > rval) {
                 new_lemma lemma(c, "x >= x0 > 0, y >= y0 > 0 => r >= x0^y0");
                 lemma |= ineq(x, llc::LT, xval);
                 lemma |= ineq(y, llc::LT, yval);
                 lemma |= ineq(r, llc::GE, r2val);
                 return l_false;
             }
-            if (xval > 0 && r2val < rval) {
-                new_lemma lemma(c, "x >= x0 > 0, y <= y0 => r <= x0^y0");
-                lemma |= ineq(x, llc::LT, xval);
+            if (r2val < rval) {
+                new_lemma lemma(c, "0 < x <= x0, y <= y0 => r <= x0^y0");
+                lemma |= ineq(x, llc::LE, rational::zero());
+                lemma |= ineq(x, llc::GT, xval);
                 lemma |= ineq(y, llc::GT, yval);
                 lemma |= ineq(r, llc::LE, r2val);
                 return l_false;

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -814,12 +814,13 @@ class theory_lra::imp {
     }
 
     lpvar get_lpvar(expr* e) {
-        return get_lpvar(get_enode(e));
+        theory_var v = mk_var(e);
+        m_solver->register_existing_terms();
+        return register_theory_var_in_lar_solver(v);
     }
 
     lpvar get_lpvar(enode* n)  {
-        ensure_column(n);
-        return n ? get_lpvar(n->get_th_var(get_id())) : lp::null_lpvar;
+        return get_lpvar(n->get_expr());
     }
 
     lpvar get_lpvar(theory_var v) const {
@@ -1674,7 +1675,6 @@ class theory_lra::imp {
             for (expr* e : m_not_handled) {
                 if (!ctx().is_relevant(e))
                     continue;
-                st = FC_DONE;
                 switch (eval_unsupported(e)) {
                 case FC_CONTINUE:
                     st = FC_CONTINUE;