mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #6585

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-02-14 15:33:17 -08:00
parent 44fcf60a72
commit a976b781a0
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/emonics.cpp
View file

@ -68,8 +68,8 @@ void emonics::pop(unsigned n) {
TRACE("nla_solver_mons", tout << "pop: " << n << "\n";); TRACE("nla_solver_mons", tout << "pop: " << n << "\n";);
SASSERT(invariant()); SASSERT(invariant());
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i) {
m_u_f_stack.pop_scope(1);
m_ve.pop(1); m_ve.pop(1);
m_u_f_stack.pop_scope(1);
} }
SASSERT(invariant()); SASSERT(invariant());
SASSERT(monics_are_canonized()); SASSERT(monics_are_canonized());

4
src/math/lp/emonics.h
View file

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