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 m_u_f; trail_stack m_u_f_stack; + union_find m_u_f; mutable svector m_find_key; // the key used when looking for a monic with the specific variables var_eqs& m_ve; mutable vector 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& ve): - m_u_f(*this), m_u_f_stack(), + m_u_f(*this), m_ve(ve), m_visited(0), m_cg_hash(*this),