* Include a few bug testcases for resolved bugs.

* Fix error message if you POP beyond the bottom user stack frame.

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 3 insertions, 2 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0a5270d83..d63a63ba2 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2447,7 +2447,7 @@ void SmtEngine::pop() throw(ModalException) {
   if(!options::incrementalSolving()) {
     throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
   }
-  if(d_userContext->getLevel() == 0) {
+  if(d_userLevels.size() == 0) {
     throw ModalException("Cannot pop beyond the first user frame");
   }
 
@@ -2457,7 +2457,8 @@ void SmtEngine::pop() throw(ModalException) {
     d_needPostsolve = false;
   }
 
-  AlwaysAssert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel());
+  AlwaysAssert(d_userContext->getLevel() > 0);
+  AlwaysAssert(d_userLevels.back() < d_userContext->getLevel());
   while (d_userLevels.back() < d_userContext->getLevel()) {
     internalPop(true);
   }