1 files changed, 3 insertions, 4 deletions
diff --git a/lib/Core/MemoryManager.cpp b/lib/Core/MemoryManager.cpp
index 06c234a2..a1198007 100644
--- a/lib/Core/MemoryManager.cpp
+++ b/lib/Core/MemoryManager.cpp
@@ -36,10 +36,9 @@ MemoryManager::~MemoryManager() {
 MemoryObject *MemoryManager::allocate(uint64_t size, bool isLocal, 
                                       bool isGlobal,
                                       const llvm::Value *allocSite) {
-  if (size>10*1024*1024) {
-    klee_warning_once(0, "failing large alloc: %u bytes", (unsigned) size);
-    return 0;
-  }
+  if (size>10*1024*1024)
+    klee_warning_once(0, "Large alloc: %u bytes.  KLEE may run out of memory.", (unsigned) size);
+  
   uint64_t address = (uint64_t) (unsigned long) malloc((unsigned) size);
   if (!address)
     return 0;