From 0d0dd0315abb337adec530c2bc17548ccea4f675 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 14 Sep 2025 06:45:36 -0700
Subject: [PATCH] evaluate unhandled arithmetic operators based on an
 initialized model #7876

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/nla_powers.cpp |  7 ++++---
 src/smt/theory_lra.cpp     | 11 +++++------
 2 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/math/lp/nla_powers.cpp b/src/math/lp/nla_powers.cpp
index 038d26fff..52c4c6e84 100644
--- a/src/math/lp/nla_powers.cpp
+++ b/src/math/lp/nla_powers.cpp
@@ -138,9 +138,10 @@ namespace nla {
         bool use_rational = !c.use_nra_model();
         rational xval, yval, rval;
         if (use_rational) {
-            xval = c.val(x);
-            yval = c.val(y);
-            rval = c.val(r);
+
+            xval = c.lra.get_value(x);
+            yval = c.lra.get_value(y);
+            rval = c.lra.get_value(r);
         } 
         else {
             auto& am = c.m_nra.am();
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 39d0df70b..0325413f4 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -186,10 +186,7 @@ class theory_lra::imp {
         imp & m_th;
         var_value_eq(imp & th):m_th(th) {}
         bool operator()(theory_var v1, theory_var v2) const { 
-            if (m_th.is_int(v1) != m_th.is_int(v2)) {
-                return false;
-            }
-            return m_th.is_eq(v1, v2);
+            return m_th.is_int(v1) == m_th.is_int(v2) && m_th.is_eq(v1, v2);
         }
     };
 
@@ -270,7 +267,6 @@ class theory_lra::imp {
             };
             m_nla->set_relevant(is_relevant);
             m_nla->updt_params(ctx().get_params());
-
         }
     }
 
@@ -470,7 +466,8 @@ class theory_lra::imp {
                     st.to_ensure_var().push_back(n1);
                     st.to_ensure_var().push_back(n2);       
                 }
-                else if (a.is_power(n, n1, n2)) {                    
+                else if (a.is_power(n, n1, n2)) { 
+                    ensure_nla();
                     found_unsupported(n);
                     if (!ctx().relevancy()) mk_power_axiom(n, n1, n2);
                     st.to_ensure_var().push_back(n1);
@@ -1680,6 +1677,8 @@ public:
             if (!int_undef && !check_bv_terms())
                 return FC_CONTINUE;
             
+            if (!m_not_handled.empty())
+                init_variable_values();
             for (expr* e : m_not_handled) {
                 if (!ctx().is_relevant(e))
                     continue;