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

catch cancellation exceptions, return undef

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-10-27 16:34:26 -07:00
parent 7d7e03e377
commit b1d673e3eb
2 changed files with 22 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/solver/combined_solver.cpp
View file

@ -21,6 +21,7 @@ Notes:
#include"solver.h" #include"solver.h"
#include"scoped_timer.h" #include"scoped_timer.h"
#include"combined_solver_params.hpp" #include"combined_solver_params.hpp"
#include"common_msgs.h"
#define PS_VB_LVL 15 #define PS_VB_LVL 15
/** /**
@ -201,7 +202,12 @@ public:
return m_solver2->get_consequences(asms, vars, consequences); return m_solver2->get_consequences(asms, vars, consequences);
} }
catch (z3_exception& ex) { catch (z3_exception& ex) {
set_reason_unknown(ex.msg()); if (get_manager().canceled()) {
set_reason_unknown(Z3_CANCELED_MSG);
}
else {
set_reason_unknown(ex.msg());
}
} }
return l_undef; return l_undef;
} }

16
src/solver/solver.cpp
View file

@ -21,6 +21,8 @@ Notes:
#include"ast_util.h" #include"ast_util.h"
#include"ast_pp.h" #include"ast_pp.h"
#include"ast_pp_util.h" #include"ast_pp_util.h"
#include "common_msgs.h"
unsigned solver::get_num_assertions() const { unsigned solver::get_num_assertions() const {
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
@ -56,7 +58,19 @@ struct scoped_assumption_push {
}; };
lbool solver::get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { lbool solver::get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
return get_consequences_core(asms, vars, consequences); try {
return get_consequences_core(asms, vars, consequences);
}
catch (z3_exception& ex) {
if (asms.get_manager().canceled()) {
set_reason_unknown(Z3_CANCELED_MSG);
return l_undef;
}
else {
set_reason_unknown(ex.msg());
}
throw;
}
} }
lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {