From 4b5fb2607f766f005c46d4ecf69620a39e5f8d94 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 24 Nov 2025 12:44:22 -1000
Subject: [PATCH] try reordering before analyzing bounds

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/nlsat/nlsat_params.pyg |  1 -
 src/nlsat/nlsat_solver.cpp | 24 +++++++++---------------
 2 files changed, 9 insertions(+), 16 deletions(-)

diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg
index 4591c4cfa..2403f94b2 100644
--- a/src/nlsat/nlsat_params.pyg
+++ b/src/nlsat/nlsat_params.pyg
@@ -8,7 +8,6 @@ def_module_params('nlsat',
                           ('cell_sample', BOOL, True, "cell sample projection"),
                           ('lazy', UINT, 0, "how lazy the solver is."),
                           ('reorder', BOOL, True, "reorder variables."),
-                          ('correct_order', BOOL, True, "apply gc/reordering before collecting branch-and-bound constraints."),
                           ('log_lemmas', BOOL, False, "display lemmas as self-contained SMT formulas"),
                           ('log_lemma_smtrat', BOOL, False, "log lemmas to be readable by smtrat"),
                           ('dump_mathematica', BOOL, False, "display lemmas as matematica"),
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 6f99164be..1283b20fe 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -214,7 +214,6 @@ namespace nlsat {
         unsigned               m_lazy;  // how lazy the solver is: 0 - satisfy all learned clauses, 1 - process only unit and empty learned clauses, 2 - use only conflict clauses for resolving conflicts
         bool                   m_simplify_cores;
         bool                   m_reorder;
-        bool                   m_correct_order;
         bool                   m_randomize;
         bool                   m_random_order;
         unsigned               m_random_seed;
@@ -293,7 +292,6 @@ namespace nlsat {
             m_simplify_cores = p.simplify_conflicts();
             bool min_cores   = p.minimize_conflicts();
             m_reorder        = p.reorder();
-            m_correct_order  = p.correct_order();
             m_randomize      = p.randomize();
             m_max_conflicts  = p.max_conflicts();
             m_random_order   = p.shuffle_vars();
@@ -1901,6 +1899,14 @@ namespace nlsat {
                        << " :learned " << m_learned.size() << ")\n");
         }
 
+        void try_reorder() {
+            gc();
+            if (m_stats.m_restarts % 10)
+                return;
+            if (m_reordered)
+                restore_order();
+            apply_reorder();            
+        }
 
         lbool search_check() {
             lbool r = l_undef;
@@ -1912,17 +1918,8 @@ namespace nlsat {
                 if (r != l_true) 
                     break; 
                 ++m_stats.m_restarts;
-                auto reorder_restart = [&]() {
-                    gc();
-                    if (m_stats.m_restarts % 10 == 0) {
-                        if (m_reordered)
-                            restore_order();
-                        apply_reorder();
-                    }
-                };
 
-                if (m_correct_order)
-                    reorder_restart();
+                try_reorder();
 
                 vector<std::pair<var, rational>> bounds;                
 
@@ -1949,9 +1946,6 @@ namespace nlsat {
                 if (bounds.empty()) 
                     break;
 
-                if (!m_correct_order)
-                    reorder_restart();
-
                 init_search();
                 IF_VERBOSE(2, verbose_stream() << "(nlsat-b&b :conflicts " << m_stats.m_conflicts 
                            << " :decisions " << m_stats.m_decisions