diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index fca2f8481..e6a3a024e 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -336,6 +336,21 @@ public:
                 catch (tactic_exception &) {
                     result.reset();
                 }
+                catch (z3_error & ex) {
+                    IF_VERBOSE(10, verbose_stream() << "z3 error: " << ex.error_code() << " in or-else\n");
+                    throw;
+                }
+                catch (z3_exception& ex) {
+                    IF_VERBOSE(10, verbose_stream() << ex.msg() << " in or-else\n");
+                    throw;
+                }
+                catch (...) {
+                    IF_VERBOSE(10, verbose_stream() << " unclassified exception in or-else\n");
+                    // std::current_exception returns a std::exception_ptr, which apparently 
+                    // needs to be re-thrown to extract type information.
+                    // typeid(ex).name() would be nice.
+                    throw;
+                }
             }
             else {
                 t->operator()(in, result);