From eb15f8249ab79e16d891d2040d9728f9f852b4ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 19 Oct 2018 21:01:25 -0700 Subject: [PATCH] fix backtrack Signed-off-by: Nikolaj Bjorner --- src/smt/theory_recfun.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index 477e8c26a..059a34f29 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -118,10 +118,11 @@ namespace smt { // restore guards unsigned new_lim = m_guard_preds_lim.size()-num_scopes; - for (unsigned i = new_lim; i < m_guard_preds.size(); ++i) { + unsigned start = m_guard_preds_lim[new_lim]; + for (unsigned i = start; i < m_guard_preds.size(); ++i) { m_guards[m_guard_preds.get(i)->get_decl()].pop_back(); } - m_guard_preds.resize(m_guard_preds_lim[new_lim]); + m_guard_preds.resize(start); m_guard_preds_lim.shrink(new_lim); }