track exceptions in reason-unknown

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Nov 19, 2024 · 5168a13 · 5168a13
1 parent a8a5069
commit 5168a13
Showing 1 changed file with 3 additions and 4 deletions.
diff --git 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()) {