diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg
index 2403f94b2..4591c4cfa 100644
--- a/src/nlsat/nlsat_params.pyg
+++ b/src/nlsat/nlsat_params.pyg
@@ -8,6 +8,7 @@ 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 0f374bfd1..6f99164be 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -214,6 +214,7 @@ 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;
@@ -292,6 +293,7 @@ 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();
@@ -1910,6 +1912,18 @@ 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();
+
                 vector<std::pair<var, rational>> bounds;                
 
                 for (var x = 0; x < num_vars(); x++) {
@@ -1935,12 +1949,8 @@ namespace nlsat {
                 if (bounds.empty()) 
                     break;
 
-                gc();
-                if (m_stats.m_restarts % 10 == 0) {
-                    if (m_reordered)
-                        restore_order();
-                    apply_reorder();
-                }
+                if (!m_correct_order)
+                    reorder_restart();
 
                 init_search();
                 IF_VERBOSE(2, verbose_stream() << "(nlsat-b&b :conflicts " << m_stats.m_conflicts