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 dc1df22a3..7a3ee0ea6 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());