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);