fix #6585

Z3Prover · Feb 14, 2023 · a976b78 · a976b78
1 parent 44fcf60
commit a976b78
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp
@@ -68,8 +68,8 @@ void emonics::pop(unsigned n) {
     TRACE("nla_solver_mons", tout << "pop: " << n << "\n";);
     SASSERT(invariant());
     for (unsigned i = 0; i < n; ++i) {
-        m_u_f_stack.pop_scope(1);
         m_ve.pop(1);
+        m_u_f_stack.pop_scope(1);
     }
     SASSERT(invariant());
     SASSERT(monics_are_canonized());

diff --git a/src/math/lp/emonics.h b/src/math/lp/emonics.h
@@ -81,8 +81,8 @@ class emonics {
         }
     };
 
-    union_find<emonics>          m_u_f;
     trail_stack                  m_u_f_stack;
+    union_find<emonics>          m_u_f;
     mutable svector<lpvar>       m_find_key; // the key used when looking for a monic with the specific variables
     var_eqs<emonics>&            m_ve;
     mutable vector<monic>        m_monics;     // set of monics
@@ -125,8 +125,8 @@ class emonics {
        other calls to push/pop to the var_eqs should take place. 
     */
     emonics(var_eqs<emonics>& ve):
-        m_u_f(*this),
         m_u_f_stack(),
+        m_u_f(*this),
         m_ve(ve), 
         m_visited(0), 
         m_cg_hash(*this),