mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

push-pop

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-10-18 15:36:48 -07:00
parent d5e5dcfe45
commit fc3a701888
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/euf_solver.cpp
View file

@ -528,6 +528,7 @@ namespace euf {
m_egraph.push(); m_egraph.push();
if (m_dual_solver) if (m_dual_solver)
m_dual_solver->push(); m_dual_solver->push();
push_relevant();
} }
void solver::pop(unsigned n) { void solver::pop(unsigned n) {
@ -537,6 +538,7 @@ namespace euf {
e->pop(n); e->pop(n);
si.pop(n); si.pop(n);
m_egraph.pop(n); m_egraph.pop(n);
pop_relevant(n);
scope const & sc = m_scopes[m_scopes.size() - n]; scope const & sc = m_scopes[m_scopes.size() - n];
for (unsigned i = m_var_trail.size(); i-- > sc.m_var_lim; ) { for (unsigned i = m_var_trail.size(); i-- > sc.m_var_lim; ) {
bool_var v = m_var_trail[i]; bool_var v = m_var_trail[i];