summaryrefslogtreecommitdiff
path: root/test/unit/context/context_mm_black.h
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/context/context_mm_black.h')
-rw-r--r--test/unit/context/context_mm_black.h5
1 files changed, 4 insertions, 1 deletions
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() {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback