diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 8e8360cd3..43093d749 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -607,7 +607,10 @@ extern "C" {
                 return Z3_L_UNDEF;
             }
             catch (...) {
-                to_solver_ref(s)->set_reason_unknown(eh);
+                if (eh.caller_id() == event_handler_caller_t::UNSET_EH_CALLER)
+                    to_solver_ref(s)->set_reason_unknown("unclassified exception");
+                else
+                    to_solver_ref(s)->set_reason_unknown(eh);
                 to_solver(s)->set_eh(nullptr);
                 return Z3_L_UNDEF;
             }
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index e6a3a024e..c5a9e6984 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -344,6 +344,10 @@ public:
                     IF_VERBOSE(10, verbose_stream() << ex.msg() << " in or-else\n");
                     throw;
                 }
+                catch (const std::exception &ex) {
+                    IF_VERBOSE(10, verbose_stream() << ex.what() << " 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