From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Thu, 15 Feb 2018 18:26:08 +0000 (-0800)
Subject: Fix context memory manager unit test (#1609)
X-Git-Tag: cvc5-1.0.0~5284
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=52a39aca19b7238d08c3cebcfa46436a73194008;p=cvc5.git

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 c789702f5..f61e76638 100644
--- 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 */
   }