From 25feb0ebedbddb9c512d86243b292dfc02238af3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 2 Apr 2022 17:43:12 -0700
Subject: [PATCH] #5938 catch also rewriter_exception that can be raised on
 cancelation and memory pressure

---
 src/tactic/arith/nla2bv_tactic.cpp | 2 +-
 src/tactic/tactical.cpp            | 3 +++
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp
index 887cc9e31..a73952be2 100644
--- a/src/tactic/arith/nla2bv_tactic.cpp
+++ b/src/tactic/arith/nla2bv_tactic.cpp
@@ -100,7 +100,7 @@ class nla2bv_tactic : public tactic {
                 return;
             }
             substitute_vars(g);
-            TRACE("nla2bv", g.display(tout << "substitute vars\n"););
+            TRACE("nla2bv", g.display(tout << "substitute vars\n"));
             reduce_bv2int(g);
             reduce_bv2real(g);
             TRACE("nla2bv", g.display(tout << "after reduce\n"););
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index 2d14a5eaa..fa9382b8c 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -336,6 +336,9 @@ public:
                 catch (tactic_exception &) {
                     result.reset();
                 }
+                catch (rewriter_exception&) {
+                    result.reset();
+                }
                 catch (z3_error & ex) {
                     IF_VERBOSE(10, verbose_stream() << "z3 error: " << ex.error_code() << " in or-else\n");
                     throw;