mirror of
https://github.com/Z3Prover/z3
synced 2025-04-11 19:53:34 +00:00
fix gcc compilation error
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
161ee1c108
commit
a6ac6958a6
|
@ -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
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue