#5986

add memory limit check to internalize
Z3Prover · Apr 19, 2022 · a1ead5f · a1ead5f
1 parent 9b66d86
commit a1ead5f
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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);
     }