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

fix bugs related to backtracking and restarts

Browse source
This commit is contained in:
Simon Cruanes 2017-12-14 20:17:11 +01:00
parent b877bd8286
commit 0c753aa86a
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_recfun.cpp
View file

@ -111,6 +111,8 @@ namespace smt {
void theory_recfun::reset_eh() { void theory_recfun::reset_eh() {
m_trail.reset(); m_trail.reset();
reset_queues(); reset_queues();
m_stats.reset();
theory::reset_eh();
} }
/* /*
@ -135,15 +137,16 @@ namespace smt {
} }
void theory_recfun::pop_scope_eh(unsigned num_scopes) { void theory_recfun::pop_scope_eh(unsigned num_scopes) {
DEBUG("pop_scope"); DEBUG("pop_scope " << num_scopes);
m_trail.pop_scope(num_scopes); m_trail.pop_scope(num_scopes);
theory::pop_scope_eh(num_scopes); theory::pop_scope_eh(num_scopes);
reset_queues(); reset_queues();
} }
void theory_recfun::restart_eh() { void theory_recfun::restart_eh() {
m_trail.reset(); DEBUG("restart");
reset_queues(); reset_queues();
theory::restart_eh();
} }
bool theory_recfun::can_propagate() { bool theory_recfun::can_propagate() {