From a6ac6958a6f2a3ae27c606fc2dbd4639260f4437 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 2 Feb 2018 09:48:02 -0800
Subject: [PATCH] fix gcc compilation error

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/util/memory_manager.cpp | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index 52046447f..7647e0989 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -11,6 +11,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "util/memory_manager.h"
 #include "util/error_codes.h"
 #include "util/z3_omp.h"
+#include "util/debug.h"
 // The following two function are automatically generated by the mk_make.py script.
 // The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
 // For example, rational.h contains
@@ -58,8 +59,6 @@ static void throw_out_of_memory() {
         g_memory_out_of_memory = true;
     }
 
-    __assume(0);
-
     if (g_exit_when_out_of_memory) {
         std::cerr << g_out_of_memory_msg << "\n";
         exit(ERR_MEMOUT);
@@ -193,9 +192,8 @@ unsigned long long memory::get_max_memory_size() {
     GlobalMemoryStatusEx (&statex);
     return statex.ullTotalPhys;
 #else
-    NOT_IMPLEMENTED_YET();
-    // two GB
-    return 1 << 31;
+    // 16 GB
+    return 1ull << 34ull;
 #endif
 }