From 7d0d7e6343b6b428ed4ac7947b2f6724a7578b22 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 19 Nov 2018 10:59:12 -0800
Subject: [PATCH] have replayer handle oom natively

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_context.cpp | 1 -
 src/api/z3_replayer.cpp | 1 +
 2 files changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index 9fe13a15f..c61fa9c4d 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -440,7 +440,6 @@ extern "C" {
     void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h) {
         RESET_ERROR_CODE();    
         mk_c(c)->set_error_handler(h);
-        // [Leo]: using exception handling, we don't need global error handlers anymore
     }
 
     void Z3_API Z3_set_error(Z3_context c, Z3_error_code e) {
diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp
index 8ebac8068..97b88c9d7 100644
--- a/src/api/z3_replayer.cpp
+++ b/src/api/z3_replayer.cpp
@@ -401,6 +401,7 @@ struct z3_replayer::imp {
 #define TICK_FREQUENCY 100000
 
     void parse() {
+        memory::exit_when_out_of_memory(false, nullptr);
         uint64_t counter = 0;
         unsigned tick = 0;
         while (true) {