fix Alive bug #875: bit blaster not respecting soft memory limit

Z3Prover · Jan 3, 2023 · e508ef1 · e508ef1
1 parent a2cc504
commit e508ef1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -27,7 +27,7 @@ Revision History:
 
 template<typename Cfg>
 void bit_blaster_tpl<Cfg>::checkpoint() {
-    if (memory::get_allocation_size() > m_max_memory)
+    if (memory::get_allocation_size() > m_max_memory || memory::above_high_watermark())
         throw rewriter_exception(Z3_MAX_MEMORY_MSG);
     if (!m().inc())
         throw rewriter_exception(m().limit().get_cancel_msg());