diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 6216d6592..f275b0ebf 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2877,6 +2877,7 @@ namespace smt {
 
     void context::push() {
         TRACE("trigger_bug", tout << "context::push()\n";);
+        scoped_suspend_rlimit _suspend_cancel(m_manager.limit());
         pop_to_base_lvl();
         setup_context(false);
         bool was_consistent = !inconsistent();
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index ad166d425..df494ec42 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -186,7 +186,7 @@ public:
     void push() override {
         switch_inc_mode();
         m_solver1->push();
-        m_solver2->push();
+        m_solver2->push();        
     }
     
     void pop(unsigned n) override {
diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp
index db745597c..41853b19a 100644
--- a/src/solver/solver_na2as.cpp
+++ b/src/solver/solver_na2as.cpp
@@ -90,9 +90,9 @@ void solver_na2as::push() {
 
 void solver_na2as::pop(unsigned n) {
     if (n > 0) {
-        pop_core(n);
         unsigned lvl = m_scopes.size();
-        SASSERT(n <= lvl);
+        n = std::min(lvl, n);
+        pop_core(n);
         unsigned new_lvl = lvl - n;
         restore_assumptions(m_scopes[new_lvl]);
         m_scopes.shrink(new_lvl);