From 98d42421bc5232bfe9a0f669d7227505bc816d37 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Jul 2018 08:42:19 -0700 Subject: [PATCH] harness more pop uses Signed-off-by: Nikolaj Bjorner --- src/solver/tactic2solver.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 135d402e6..85d3b483d 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -125,6 +125,7 @@ void tactic2solver::push_core() { } void tactic2solver::pop_core(unsigned n) { + n = std::min(m_scopes.size(), n); unsigned new_lvl = m_scopes.size() - n; unsigned old_sz = m_scopes[new_lvl]; m_assertions.shrink(old_sz); @@ -142,9 +143,8 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass m_tactic->updt_params(get_params()); // parameters are allowed to overwrite logic. goal_ref g = alloc(goal, m, m_produce_proofs, m_produce_models, m_produce_unsat_cores); - unsigned sz = m_assertions.size(); - for (unsigned i = 0; i < sz; i++) { - g->assert_expr(m_assertions.get(i)); + for (expr* e : m_assertions) { + g->assert_expr(e); } for (unsigned i = 0; i < num_assumptions; i++) { proof_ref pr(m.mk_asserted(assumptions[i]), m);