diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 97cac90fc..5bc0d214f 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -333,7 +333,7 @@ namespace nlsat { void checkpoint() { if (!m_rlimit.inc()) throw solver_exception(m_rlimit.get_cancel_msg()); - if (memory::get_allocation_size() > m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG); + if (memory::get_allocation_size()/(1 << 20) > m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG); } // -----------------------