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;