From 823800541eb969a1ec9237102cd1d7401f683c33 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 19 Nov 2025 14:02:27 -0800
Subject: [PATCH] updates

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/nla_order_lemmas.cpp |  2 ++
 src/math/lp/nra_solver.cpp       |  9 ++++++---
 src/nlsat/nlsat_solver.cpp       | 28 ++++++++++++++++------------
 3 files changed, 24 insertions(+), 15 deletions(-)

diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp
index 37e8f3f19..30fb89f3d 100644
--- a/src/math/lp/nla_order_lemmas.cpp
+++ b/src/math/lp/nla_order_lemmas.cpp
@@ -24,6 +24,8 @@ void order::order_lemma() {
         TRACE(nla_solver, tout << "not generating order lemmas\n";);
         return;
     }
+    if (!c().params().arith_nl_linearize())
+        return;
    
     for (auto j : c().m_to_refine) {
         if (done()) break; 
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 4ec0e7812..5f6b8f276 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -129,6 +129,7 @@ struct solver::imp {
             }
             auto lit = add_constraint(p, ci, k);
         }
+        definitions.reset();
     }
 
     void setup_solver_terms() {
@@ -153,10 +154,10 @@ struct solver::imp {
                 continue;
             auto value = m_nla_core.val(v);
             SASSERT(value.is_int());
-            unsigned sz = m_model_bounds.size();
+            unsigned offset = m_model_bounds.size() + m_max_constraint_index;
             m_model_bounds.push_back({v, value, true});
             m_model_bounds.push_back({v, value, false});
-            m_nlsat->track_model_value(lp2nl(v), value, this + sz, this + sz + 1);
+            m_nlsat->track_model_value(lp2nl(v), value, this + offset, this + offset + 1);
         }
     }
 
@@ -174,7 +175,7 @@ struct solver::imp {
     lbool check() {
         SASSERT(need_check());
         reset();
-        vector<nlsat::assumption, false> core;
+        vector<nlsat::assumption, false> core;        
         
         smt_params_helper p(m_params);
 
@@ -250,6 +251,7 @@ struct solver::imp {
             nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
             for (auto c : core) {
                 unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this);
+                TRACE(nra, tout << "core index " << idx << " " << m_max_constraint_index << "\n");
                 if (idx <= m_max_constraint_index)
                     ex.push_back(idx);
                 else {
@@ -360,6 +362,7 @@ struct solver::imp {
     }
 
     nlsat::literal add_constraint(polynomial::polynomial *p, unsigned idx, lp::lconstraint_kind k) {
+        m_max_constraint_index = std::max(m_max_constraint_index, idx);
         polynomial::polynomial *ps[1] = {p};
         bool is_even[1] = {false};
         nlsat::literal lit;
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 62490f1bc..82088d76c 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -1871,6 +1871,7 @@ namespace nlsat {
 
 
         lbool search_check() {
+            verbose_stream() << "search check\n";
             lbool r = l_undef;
             m_stats.m_conflicts = 0;
             m_stats.m_restarts = 0;
@@ -1880,8 +1881,15 @@ namespace nlsat {
                 if (r != l_true) 
                     break; 
                 ++m_stats.m_restarts;
-                vector<std::pair<var, rational>> bounds;                
 
+                gc();
+                if (m_stats.m_restarts % 10 == 0) {
+                    if (m_reordered)
+                        restore_order();
+                    apply_reorder();
+                }
+
+                vector<std::pair<var, rational>> bounds;                
                 for (var x = 0; x < num_vars(); x++) {
                     if (is_int(x) && m_assignment.is_assigned(x) && !m_am.is_int(m_assignment.value(x))) {
                         scoped_anum v(m_am), vlo(m_am);
@@ -1905,13 +1913,6 @@ namespace nlsat {
                 if (bounds.empty()) 
                     break;
 
-                gc();
-                if (m_stats.m_restarts % 10 == 0) {
-                    if (m_reordered)
-                        restore_order();
-                    apply_reorder();
-                }
-
                 init_search();
                 IF_VERBOSE(2, verbose_stream() << "(nlsat-b&b :conflicts " << m_stats.m_conflicts 
                            << " :decisions " << m_stats.m_decisions 
@@ -1925,15 +1926,18 @@ namespace nlsat {
                 if (!m_model_values.empty()) {
                     bool found = false;
                     random_gen r(++m_random_seed);
-                    auto const &[x, bound] = bounds[r(bounds.size())];
-                        for (auto const &[mx, mvalue, lo, hi] : m_model_values) {
-                        if (mx == x) {
+                    auto const &[x, value] = bounds[r(bounds.size())];
+                    for (auto const &[ext_x, mvalue, lo, hi] : m_model_values) {
+                        if (ext_x == m_perm[x]) {
+                            verbose_stream() << x << " " << ext_x << " bound: " << mvalue << " value " << value
+                                             << "\n ";
+                            TRACE(nla_solver, tout << "x" << ext_x << " bound " << mvalue << "\n");
                             polynomial_ref p(m_pm);
                             rational one(1);
                             bool is_even = false;
                             p = m_pm.mk_linear(1, &one, &x, -mvalue);  // x - mvalue
                             auto *p1 = p.get();
-                            if (mvalue < bound) {
+                            if (mvalue < value) {
                                 // assert x <= mvalue
                                 // <=>
                                 // ~ (x > mvalue)