From 8be43ca68b1b8de55a6b92692a4544d711489016 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 25 Jan 2023 13:51:19 -0800
Subject: [PATCH] reshuffle pre-conditions for powers

---
 src/math/lp/nla_powers.cpp | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/math/lp/nla_powers.cpp b/src/math/lp/nla_powers.cpp
index ee3c41ee894..847ef7a84a3 100644
--- a/src/math/lp/nla_powers.cpp
+++ b/src/math/lp/nla_powers.cpp
@@ -83,6 +83,8 @@ namespace nla {
             return l_undef;
 
         core& c = m_core;        
+        if (c.use_nra_model()) 
+            return l_undef;
 
         auto xval = c.val(x);
         auto yval = c.val(y);
@@ -90,7 +92,6 @@ namespace nla {
 
         lemmas.reset();
 
-
         if (xval != 0 && yval == 0 && rval != 1) {
             new_lemma lemma(c, "x != 0 => x^0 = 1");
             lemma |= ineq(x, llc::EQ, rational::zero());
@@ -99,7 +100,7 @@ namespace nla {
             return l_false;
         }
 
-        if (xval == 0 && yval > 0 && rval != 0) {
+        if (xval == 0 && yval != 0 && rval != 0) {
             new_lemma lemma(c, "y != 0 => 0^y = 0");
             lemma |= ineq(x, llc::NE, rational::zero());
             lemma |= ineq(y, llc::EQ, rational::zero());
@@ -107,14 +108,14 @@ namespace nla {
             return l_false;
         }
 
-        if (xval > 0 && rval < 0 && rval <= 0) {
+        if (xval > 0 && rval <= 0) {
             new_lemma lemma(c, "x > 0 => x^y > 0");
             lemma |= ineq(x, llc::LE, rational::zero());
             lemma |= ineq(r, llc::GT, rational::zero());
             return l_false;
         }
 
-        if (xval > 1 && rval >= 1 && yval < 0) {
+        if (xval > 1 && yval < 0 && rval >= 1) {
             new_lemma lemma(c, "x > 1, y < 0 => x^y < 1");
             lemma |= ineq(x, llc::LE, rational::one());
             lemma |= ineq(y, llc::GE, rational::zero());
@@ -122,7 +123,7 @@ namespace nla {
             return l_false;
         }
 
-        if (xval > 1 && rval <= 1 && yval > 0) {
+        if (xval > 1 && yval > 0 && rval <= 1) {
             new_lemma lemma(c, "x > 1, y > 0 => x^y > 1");
             lemma |= ineq(x, llc::LE, rational::one());
             lemma |= ineq(y, llc::LE, rational::zero());