Fix context memory manager unit test (#1609)

Commit 83f150c727f197c530d6f46a75b516eea52bed29 changed the flag
that we use to determine whether to use the context memory manager
or the debug version. However, the change was not reflected in
the context memory manager unit test. This commit fixes the unit
test to check the correct flag.

diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h
index c789702f5b7be3dccd2fe1478b2827948e9dc005..f61e76638db15499cf52683b93c1965118b76bc6 100644 (file)
--- a/test/unit/context/context_mm_black.h
+++ b/test/unit/context/context_mm_black.h
@@ -40,7 +40,9 @@ public:
   }
 
   void testPushPop() {
-#ifdef CVC4_CONTEXT_MEMORY_MANAGER
+#ifdef CVC4_DEBUG_CONTEXT_MEMORY_MANAGER
+#warning "Using the debug context memory manager, omitting unit tests"
+#else
     // Push, then allocate, then pop
     // We make sure that we don't allocate too much so that all the regions
     // should be reclaimed
@@ -91,8 +93,6 @@ public:
 
     // Try popping out of scope
     TS_ASSERT_THROWS(d_cmm->pop(), CVC4::AssertionException);
-#else /* CVC4_CONTEXT_MEMORY_MANAGER */
-#warning "Context memory manager disabled, omitting unit tests"
 #endif /* __CVC4__CONTEXT__CONTEXT_MM_H */
   }