diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 4a151bb37..8f3f91888 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -164,6 +164,7 @@ namespace opt {
     }
 
     void context::pop(unsigned n) {
+        n = std::min(n, m_scoped_state.num_scopes());
         for (unsigned i = 0; i < n; ++i) {
             m_scoped_state.pop();
         }
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 3d0c872df..27d0eb791 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -133,6 +133,7 @@ namespace opt {
                 m_hard(m),
                 m_asms(m)
             {}
+            unsigned num_scopes() const { return m_hard_lim.size(); }
             void push();
             void pop();
             void add(expr* hard);