From 78ebe0a94c65c8de06270b2ba406630230099929 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 2 Apr 2020 06:22:32 -0700
Subject: [PATCH] fix #3701

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/solver/solver_na2as.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp
index 4f284a2d6..845973dbf 100644
--- a/src/solver/solver_na2as.cpp
+++ b/src/solver/solver_na2as.cpp
@@ -90,7 +90,7 @@ void solver_na2as::push() {
 }
 
 void solver_na2as::pop(unsigned n) {
-    if (n > 0) {
+    if (n > 0 && !m_scopes.empty()) { 
         unsigned lvl = m_scopes.size();
         n = std::min(lvl, n);
         pop_core(n);