Merge pull request #100 from 4tXJ7f/fix_context_mm_black

Fix back() of empty deque in context_mm_black test

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() {