From 5d316a51d1eb76861c10677221e3222293bb649d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 19 Nov 2025 10:53:42 -0800
Subject: [PATCH] enable bound tracking

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

diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 6e233514d..4ec0e7812 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -156,7 +156,7 @@ struct solver::imp {
             unsigned sz = m_model_bounds.size();
             m_model_bounds.push_back({v, value, true});
             m_model_bounds.push_back({v, value, false});
-            m_nlsat->track_model_value(v, value, this + sz, this + sz + 1);
+            m_nlsat->track_model_value(lp2nl(v), value, this + sz, this + sz + 1);
         }
     }
 
@@ -255,6 +255,7 @@ struct solver::imp {
                 else {
                     idx -= m_max_constraint_index;
                     auto const& [v, bound, is_lower] = m_model_bounds[idx];
+                    TRACE(nra, tout << "bound violated for v" << v << (is_lower ? " >= " : " <= ") << bound << "\n");
                     if (is_lower)
                         lemma |= nla::ineq(v, lp::lconstraint_kind::LE, bound - 1);
                     else
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 2016d19bc..62490f1bc 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -1920,34 +1920,37 @@ namespace nlsat {
                            << " :learned " << m_learned.size() << ")\n");
 
 
-                #if 0
                 // todo, review, test
                 // cut on the first model value
                 if (!m_model_values.empty()) {
                     bool found = false;
-                    for (auto const &[x, bound] : bounds) {
+                    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) {
-                                polynomial_ref p(m_pm);
-                                rational one(1);
-                                bool is_even = false;
-                                p = m_pm.mk_linear(1, &one, &x, mvalue);
-                                auto* p1 = p.get();
-                                if (mvalue < bound) {
-                                    mk_external_clause(1, &mk_ineq_literal(atom::GT, 1, &p1, &is_even), assumption(lo));
-                                }
-                                else {
-                                    mk_external_clause(1, &mk_ineq_literal(atom::LT, 1, &p1, &is_even), assumption(hi));
-                                }
-                                found = true;
-                                break;
+                        if (mx == x) {
+                            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) {
+                                // assert x <= mvalue
+                                // <=>
+                                // ~ (x > mvalue)
+                                // assumption hi
+                                auto lit = ~mk_ineq_literal(atom::GT, 1, &p1, &is_even);
+                                mk_external_clause(1, &lit, assumption(hi));
                             }
-                        }
-                        if (found)
+                            else {
+                                auto lit = ~mk_ineq_literal(atom::LT, 1, &p1, &is_even);
+                                mk_external_clause(1, &lit, assumption(lo));
+                            }
+                            found = true;
                             break;
+                        }                        
                     }
+                    continue;
                 }
-                #endif
                 for (auto const& b : bounds) {
                     var x = b.first;
                     rational lo = b.second;