From e508ef17f6d6d716f88906d7f7acb35bece9bc92 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Tue, 3 Jan 2023 10:39:28 +0000
Subject: [PATCH] fix Alive bug #875: bit blaster not respecting soft memory
 limit

---
 src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h | 2 +-
 1 file changed, 1 insertion(+), 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
index dc1df22a362..7a3ee0ea619 100644
--- 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());