diff options
author | Tim King <taking@cs.nyu.edu> | 2016-11-03 08:32:27 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-11-03 08:32:27 -0700 |
commit | 8a8455d955c084c9a9f7add1f4e4da6b1dbc35eb (patch) | |
tree | 008e517455ecfcdfa3d25a17d2ba73a9638d0593 | |
parent | f1427165156dff24d7b8ca0690088e4182ccdbd4 (diff) | |
parent | 520e4a0638675dad2fa66a50e5fd64786c6f889f (diff) |
Merge pull request #100 from 4tXJ7f/fix_context_mm_black
Fix back() of empty deque in context_mm_black test
-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() { |