diff --git a/src/util/lp/var_eqs.cpp b/src/util/lp/var_eqs.cpp
index 0a422c254..16708180a 100644
--- a/src/util/lp/var_eqs.cpp
+++ b/src/util/lp/var_eqs.cpp
@@ -27,7 +27,7 @@ var_eqs::var_eqs(): m_merge_handler(nullptr), m_uf(*this), m_stack(*this) {}
     
 void var_eqs::push() {
     m_trail_lim.push_back(m_trail.size());
-    get_trail_stack().push_scope();
+    m_stack.push_scope();
 }
 
 void var_eqs::pop(unsigned n) {
@@ -41,7 +41,7 @@ void var_eqs::pop(unsigned n) {
     }
     m_trail_lim.shrink(m_trail_lim.size() - n);
     m_trail.shrink(old_sz);
-    get_trail_stack().pop_scope(n);
+    m_stack.pop_scope(n);
 }
 
 void var_eqs::merge(signed_var v1, signed_var v2, eq_justification const& j) {
diff --git a/src/util/lp/var_eqs.h b/src/util/lp/var_eqs.h
index 32c30503c..df673f163 100644
--- a/src/util/lp/var_eqs.h
+++ b/src/util/lp/var_eqs.h
@@ -180,6 +180,7 @@ public:
 
     // union find event handlers
     void set_merge_handler(var_eqs_merge_handler* mh) { m_merge_handler = mh; }
+    // this method is required by union_find
     trail_stack<var_eqs> & get_trail_stack() { return m_stack; }
 
     void unmerge_eh(unsigned i, unsigned j) { 
@@ -200,9 +201,8 @@ public:
                                             signed_var(v2), signed_var(v1)); 
         }
     }
+};  // end of var_eqs
 
+inline std::ostream& operator<<(var_eqs const& ve, std::ostream& out) { return ve.display(out); }
 
-}; 
-
-    inline std::ostream& operator<<(var_eqs const& ve, std::ostream& out) { return ve.display(out); }
 }