From a5488cf6e7bb4623d4120d1b59c06c6cdd952280 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 30 Nov 2025 07:51:06 -0800
Subject: [PATCH] fix #8054

inherit denominators when evaluating polynomials
---
 src/math/lp/nra_solver.cpp | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 63f16f8ef..f083c0f82 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -65,6 +65,7 @@ struct solver::imp {
         if (m_nla_core.emons().is_monic_var(v)) {
             auto const &m = m_nla_core.emons()[v];
             for (auto v2 : m.vars()) {
+                den = lcm(denominators[v2], den);
                 polynomial_ref pw(definitions.get(v2), m_nlsat->pm());
                 if (!p)
                     p = pw;
@@ -74,7 +75,7 @@ struct solver::imp {
         }
         else if (lra.column_has_term(v)) {
             for (auto const &[w, coeff] : lra.get_term(v)) {
-                den = lcm(denominator(coeff), den);
+                den = lcm(denominators[w], lcm(denominator(coeff), den));
             }
             for (auto const &[w, coeff] : lra.get_term(v)) {
                 auto coeff1 = den * coeff;
@@ -128,7 +129,7 @@ struct solver::imp {
                 poly = poly * constant(den * coeff / denominators[v]);
                 p = p + poly;
             }
-           add_constraint(p, ci, k);
+            add_constraint(p, ci, k);
         }
         definitions.reset();
     }
@@ -223,6 +224,7 @@ struct solver::imp {
               for (auto [j, x] : m_lp2nl) tout << "j" << j << " := x" << x << "\n";);
         switch (r) {
         case l_true:
+            m_nlsat->restore_order();
             m_nla_core.set_use_nra_model(true);
             lra.init_model();
             for (lp::constraint_index ci : lra.constraints().indices())
@@ -427,6 +429,7 @@ struct solver::imp {
         
         switch (r) {
         case l_true:
+            m_nlsat->restore_order();
             m_nla_core.set_use_nra_model(true);
             lra.init_model();
             for (lp::constraint_index ci : lra.constraints().indices())
@@ -628,9 +631,10 @@ struct solver::imp {
         unsigned w;
         scoped_anum a(am());
         for (unsigned v = m_values->size(); v < sz; ++v) {
-            if (m_nla_core.emons().is_monic_var(v)) {
+            if (m_nla_core.emons().is_monic_var(v)) {                 
                 am().set(a, 1);
                 auto &m = m_nla_core.emon(v);
+
                 for (auto x : m.vars()) 
                     am().mul(a, (*m_values)[x], a);
                 m_values->push_back(a);
@@ -638,7 +642,7 @@ struct solver::imp {
             else if (lra.column_has_term(v)) {
                 scoped_anum b(am());
                 am().set(a, 0);
-                for (auto const &[w, coeff] : lra.get_term(v)) {
+                for (auto const &[w, coeff] : lra.get_term(v)) {                    
                     am().set(b, coeff.to_mpq());
                     am().mul(b, (*m_values)[w], b);
                     am().add(a, b, a);