mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

add exception handling to easier diagnose #7418

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-11-19 11:46:54 -08:00
parent 5168a13efa
commit e855a50d9b
3 changed files with 17 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/api/api_solver.cpp
View file

@ -655,7 +655,7 @@ extern "C" {
result = to_solver_ref(s)->check_sat(num_assumptions, _assumptions);
}
catch (z3_exception & ex) {
to_solver_ref(s)->set_reason_unknown(eh);
to_solver_ref(s)->set_reason_unknown(eh, ex);
to_solver(s)->set_eh(nullptr);
if (mk_c(c)->m().inc()) {
mk_c(c)->handle_exception(ex);
@ -751,8 +751,8 @@ extern "C" {
try {
to_solver_ref(s)->get_unsat_core(core);
}
catch (...) {
to_solver_ref(s)->set_reason_unknown(eh);
catch (std::exception& ex) {
to_solver_ref(s)->set_reason_unknown(eh, ex);
to_solver(s)->set_eh(nullptr);
if (core.empty())
throw;
@ -877,7 +877,7 @@ extern "C" {
}
catch (z3_exception & ex) {
to_solver(s)->set_eh(nullptr);
to_solver_ref(s)->set_reason_unknown(eh);
to_solver_ref(s)->set_reason_unknown(eh, ex);
_assumptions.finalize(); _consequences.finalize(); _variables.finalize();
mk_c(c)->handle_exception(ex);
return Z3_L_UNDEF;