diff options
Diffstat (limited to 'src/context/context_mm.cpp')
-rw-r--r-- | src/context/context_mm.cpp | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index db9d89dd1..4d9413320 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -15,9 +15,11 @@ **/ #include <cstdlib> -#include <vector> #include <deque> +#include <limits> #include <new> +#include <ostream> +#include <vector> #ifdef CVC4_VALGRIND #include <valgrind/memcheck.h> @@ -166,6 +168,12 @@ void ContextMemoryManager::pop() { d_freeChunks.pop_front(); } } +#else + +unsigned ContextMemoryManager::getMaxAllocationSize() +{ + return std::numeric_limits<unsigned>::max(); +} #endif /* CVC4_DEBUG_CONTEXT_MEMORY_MANAGER */ |