diff options
| -rw-r--r-- | src/context/context_mm.cpp | 2 | ||||
| -rw-r--r-- | test/unit/context/context_mm_black.h | 5 |
2 files changed, 6 insertions, 1 deletions
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index 2dc2c03bb..ac7d7f8cf 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -104,6 +104,8 @@ void ContextMemoryManager::push() { void ContextMemoryManager::pop() { + Assert(d_nextFreeStack.size() > 0 && d_endChunkStack.size() > 0); + // Restore state from stack d_nextFree = d_nextFreeStack.back(); d_nextFreeStack.pop_back(); diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h index 60671653c..00a0fd05f 100644 --- a/test/unit/context/context_mm_black.h +++ b/test/unit/context/context_mm_black.h @@ -20,8 +20,11 @@ //Used in some of the tests #include <vector> #include <iostream> + #include "context/context_mm.h" +#include "base/cvc4_assert.h" + using namespace std; using namespace CVC4::context; @@ -87,7 +90,7 @@ public: } // Try popping out of scope - d_cmm->pop(); + TS_ASSERT_THROWS(d_cmm->pop(), CVC4::AssertionException); } void tearDown() { |