From a976b781a04e26abf763b2f8029c98a7b0a294b7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 14 Feb 2023 15:33:17 -0800
Subject: [PATCH] fix #6585

---
 src/math/lp/emonics.cpp | 2 +-
 src/math/lp/emonics.h   | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp
index 21bfe6792..bcdb81dd8 100644
--- 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
index d26d96ad6..e4f4f4848 100644
--- 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 @@ public:
        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),