track exceptions in reason-unknown

NikolajBjorner · NikolajBjorner · commit 5168a13efacf · 2024-11-19T09:29:23.000-08:00
Signed-off-by: Nikolaj Bjorner &lt;nbjorner@microsoft.com&gt;
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()) {

Original file line number	Diff line number	Diff line change
`@@ -317,10 +317,9 @@ lbool solver::check_sat(unsigned num_assumptions, expr * const * assumptions) {`
`317`	`317`	`try {`
`318`	`318`	`r = check_sat_core(num_assumptions, assumptions);`
`319`	`319`	`}`
`320`		`- catch (...) {`
`321`		`- if (!get_manager().limit().inc(0)) {`
`322`		`- dump_state(num_assumptions, assumptions);`
`323`		`- }`
	`320`	`+ catch (std::exception& ex) {`
	`321`	`+ if (reason_unknown() == "")`
	`322`	`+ set_reason_unknown(ex.what());`
`324`	`323`	`throw;`
`325`	`324`	`}`
`326`	`325`	`if (r == l_undef && !get_manager().inc()) {`