From 52a39aca19b7238d08c3cebcfa46436a73194008 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 15 Feb 2018 10:26:08 -0800 Subject: [PATCH] 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. --- test/unit/context/context_mm_black.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 */ } -- 2.30.2