mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 17:36:15 +00:00
Code Activity

more detailed tracing of where unmaterialized exceptions happen

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-11-19 18:15:42 -08:00
parent 7de0c29f12
commit 012fc1b72b
4 changed files with 14 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/cmd_context/cmd_context.cpp
View file

@ -1782,19 +1782,15 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
try {
r = m_solver->check_sat(num_assumptions, assumptions);
if (r == l_undef && !m().inc()) {
m_solver->set_reason_unknown(eh);
m_solver->set_reason_unknown(eh, "canceled");
}
}
catch (z3_error & ex) {
m_solver->set_reason_unknown(eh, ex);
throw ex;
}
catch (z3_exception & ex) {
if (!m().inc()) {
m_solver->set_reason_unknown(eh);
}
else {
m_solver->set_reason_unknown(ex.what());
}
m_solver->set_reason_unknown(eh, ex);
r = l_undef;
}
m_solver->set_status(r);