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 */