diff --git a/src/util/env_params.cpp b/src/util/env_params.cpp index 28d80d92d..b01a1c250 100644 --- a/src/util/env_params.cpp +++ b/src/util/env_params.cpp @@ -26,7 +26,7 @@ void env_params::updt_params() { params_ref p = gparams::get(); set_verbosity_level(p.get_uint("verbose", get_verbosity_level())); enable_warning_messages(p.get_bool("warning", true)); - memory::set_max_size(p.get_uint("memory_max_size", 0)); + memory::set_max_size(megabytes_to_bytes(p.get_uint("memory_max_size", 0))); memory::set_high_watermark(p.get_uint("memory_high_watermark", 0)); } diff --git a/src/util/util.h b/src/util/util.h index 3360c2282..8bcbce4a3 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -394,11 +394,14 @@ public: inline std::ostream & operator<<(std::ostream & out, escaped const & s) { s.display(out); return out; } -inline unsigned long long megabytes_to_bytes(unsigned b) { - if (b == UINT_MAX) - return UINT64_MAX; - else - return static_cast(b) * 1024ull * 1024ull; +inline size_t megabytes_to_bytes(unsigned mb) { + if (mb == UINT_MAX) + return SIZE_MAX; + unsigned long long b = static_cast(mb) * 1024ull * 1024ull; + size_t r = static_cast(b); + if (r != b) // overflow + r = SIZE_MAX; + return r; } void z3_bound_num_procs();