From 5168a13efacf2ecd39654be04d6b577424b9b8b0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 19 Nov 2024 09:28:13 -0800
Subject: [PATCH] track exceptions in reason-unknown

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/solver/solver.cpp | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

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()) {