fix #6590

Z3Prover · Feb 15, 2023 · 8ce0c56 · 8ce0c56
1 parent c2fe765
commit 8ce0c56
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/math/lp/nla_powers.cpp b/src/math/lp/nla_powers.cpp
@@ -81,6 +81,8 @@ namespace nla {
     lbool powers::check(lpvar r, lpvar x, lpvar y, vector<lemma>& lemmas) {
         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))
+            return l_undef;
 
         core& c = m_core;        
         if (c.use_nra_model())