From 0c753aa86ac908af28703a5885a50ddd0e0ce6d1 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 14 Dec 2017 20:17:11 +0100 Subject: [PATCH] fix bugs related to backtracking and restarts --- src/smt/theory_recfun.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index fdbdeac47..a910a62ef 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -111,6 +111,8 @@ namespace smt { void theory_recfun::reset_eh() { m_trail.reset(); reset_queues(); + m_stats.reset(); + theory::reset_eh(); } /* @@ -135,15 +137,16 @@ namespace smt { } void theory_recfun::pop_scope_eh(unsigned num_scopes) { - DEBUG("pop_scope"); + DEBUG("pop_scope " << num_scopes); m_trail.pop_scope(num_scopes); theory::pop_scope_eh(num_scopes); reset_queues(); } void theory_recfun::restart_eh() { - m_trail.reset(); + DEBUG("restart"); reset_queues(); + theory::restart_eh(); } bool theory_recfun::can_propagate() {