diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index 8437f92cc..baca06421 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -317,10 +317,9 @@ lbool solver::check_sat(unsigned num_assumptions, expr * const * assumptions) {
     try {
         r = check_sat_core(num_assumptions, assumptions);
     }
-    catch (...) {
-        if (!get_manager().limit().inc(0)) {
-            dump_state(num_assumptions, assumptions);
-        }
+    catch (std::exception& ex) {
+        if (reason_unknown() == "")
+            set_reason_unknown(ex.what());
         throw;
     }
     if (r == l_undef && !get_manager().inc()) {