mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-20 02:00:22 +00:00
Code Activity

fix #7792

Browse source 
add missing revert operations
This commit is contained in:
Nikolaj Bjorner 2025-08-17 17:08:27 -07:00
parent ff74af7eaa
commit 7ff0b246e8
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/simplifiers/model_reconstruction_trail.cpp
View file

@ -80,6 +80,7 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt
add_vars(v, free_vars); add_vars(v, free_vars);
st.add(dependent_expr(m, m.mk_eq(k, v), nullptr, nullptr)); st.add(dependent_expr(m, m.mk_eq(k, v), nullptr, nullptr));
} }
m_trail_stack.push(value_trail(t->m_active));
t->m_active = false; t->m_active = false;
continue; continue;
} }
@ -90,6 +91,7 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt
TRACE(simplifier, tout << "replay removed " << r << "\n"); TRACE(simplifier, tout << "replay removed " << r << "\n");
st.add(r); st.add(r);
} }
m_trail_stack.push(value_trail(t->m_active));
t->m_active = false; t->m_active = false;
continue; continue;
} }