diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index ec58a1500..e5a398362 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -636,6 +636,9 @@ void core::erase_from_to_refine(lpvar j) {
 void core::init_to_refine() {
     TRACE(nla_solver_details, tout << "emons:" << pp_emons(*this, m_emons););
     m_to_refine.reset();
+    // Traversal order of monomials uses randomization to avoid bias.
+    // We can cache a shuffle of m_emons indices instead of using cyclic shifts
+    // The shuffle can survive backtracking points to enforce bias within a scope.
     unsigned r = random(), sz = m_emons.number_of_monics();
     for (unsigned k = 0; k < sz; k++) {
         auto const & m = *(m_emons.begin() + (k + r)% sz);
@@ -812,9 +815,7 @@ bool core::find_bfc_to_refine_on_monic(const monic& m, factorization & bf) {
 // finds a monic to refine with its binary factorization
 bool core::find_bfc_to_refine(const monic* & m, factorization & bf){
     m = nullptr;
-    unsigned r = random(), sz = m_to_refine.size();
-    for (unsigned k = 0; k < sz; k++) {
-        lpvar i = m_to_refine[(k + r) % sz];
+    for (auto i : m_to_refine) {
         m = &m_emons[i];
         SASSERT (!check_monic(*m));
         if (has_real(m))
@@ -1213,16 +1214,9 @@ void core::patch_monomials_on_to_refine() {
     // the rest of the function might change m_to_refine, so have to copy
     unsigned_vector to_refine;
     for (unsigned j : m_to_refine) 
-        to_refine.push_back(j);
-    
-    unsigned sz = to_refine.size();
-
-    unsigned start = random();
-    for (unsigned i = 0; i < sz && !m_to_refine.empty(); i++) 
-        patch_monomial(to_refine[(start + i) % sz]);
-
-    TRACE(nla_solver, tout << "sz = " << sz << ", m_to_refine = " << m_to_refine.size() <<
-          (sz > m_to_refine.size()? " less" : " same" ) << "\n";);
+        to_refine.push_back(j);    
+    for (auto j : to_refine)
+        patch_monomial(j);
 }
 
 void core::patch_monomials() {
@@ -1265,9 +1259,7 @@ void core::check_bounded_divisions() {
 }
 // looking for a free variable inside of a monic to split
 void core::add_bounds() {
-    unsigned r = random(), sz = m_to_refine.size();
-    for (unsigned k = 0; k < sz; k++) {
-        lpvar i = m_to_refine[(k + r) % sz];
+    for (auto i : m_to_refine) {
         auto const& m = m_emons[i];
         for (lpvar j : m.vars()) {
             if (!var_is_free(j))
diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp
index be5a82ffa..f2f05571e 100644
--- a/src/math/lp/nla_monotone_lemmas.cpp
+++ b/src/math/lp/nla_monotone_lemmas.cpp
@@ -12,10 +12,8 @@ namespace nla {
 monotone::monotone(core * c) : common(c) {}
     
 void monotone::monotonicity_lemma() {
-    unsigned shift = random();
-    unsigned size = c().m_to_refine.size();
-    for (unsigned i = 0; i < size && !done(); i++) { 
-        lpvar v = c().m_to_refine[(i + shift) % size];
+    for (auto v : c().m_to_refine) {
+        if (done()) break;
         monotonicity_lemma(c().emons()[v]);
     }
 }
diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp
index 81714f697..4731ec867 100644
--- a/src/math/lp/nla_order_lemmas.cpp
+++ b/src/math/lp/nla_order_lemmas.cpp
@@ -23,12 +23,9 @@ void order::order_lemma() {
         TRACE(nla_solver, tout << "not generating order lemmas\n";);
         return;
     }
-    
-    const auto& to_ref = c().m_to_refine;
-    unsigned r = random();
-    unsigned sz = to_ref.size();
-    for (unsigned i = 0; i < sz && !done(); ++i) {
-        lpvar j = to_ref[(i + r) % sz];
+   
+    for (auto j : c().m_to_refine) {
+        if (done()) break; 
         order_lemma_on_monic(c().emons()[j]);
     }
 }