diff options
Diffstat (limited to 'src/context/context_mm.cpp')
| -rw-r--r-- | src/context/context_mm.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index 39af8bd9e..a36d523f7 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -74,7 +74,7 @@ ContextMemoryManager::ContextMemoryManager() : d_indexChunkList(0) { #ifdef CVC4_VALGRIND VALGRIND_CREATE_MEMPOOL(this, 0, false); VALGRIND_MAKE_MEM_NOACCESS(d_nextFree, chunkSizeBytes); - d_allocations.push_back(std::vector<void*>()); + d_allocations.push_back(std::vector<char*>()); #endif /* CVC4_VALGRIND */ } |