From a1ead5f47d4f596f7f59202cf6f8752c8e165b2a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 19 Apr 2022 07:31:40 +0200
Subject: [PATCH] #5986

add memory limit check to internalize
---
 src/smt/smt_internalizer.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index fd55d5fd0..eee811e62 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -350,6 +350,8 @@ namespace smt {
        - gate_ctx is true if the expression is in the context of a logical gate.
     */
     void context::internalize(expr * n, bool gate_ctx) {
+        if (memory::above_high_watermark())
+            throw default_exception("resource limit exceeded during internalization");
         internalize_deep(n);
         internalize_rec(n, gate_ctx);
     }