Fix back() of empty deque in context_mm_black test

The `testPushPop()` test case does a pop out of scope at the end that
lead to UB in `ContextManager::pop()` because it did a `deque::back()`
on an empty deque without checking. This commit adds an assertion in the
`ContextManager` and checks that the test case triggers the assertion.

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