mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #5271

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-17 10:42:34 -07:00
parent 93a9847815
commit d2bd92eab9
2 changed files with 25 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/smt/smt_model_checker.cpp
View file

@ -319,7 +319,14 @@ namespace smt {
struct scoped_ctx_push { struct scoped_ctx_push {
context* c; context* c;
scoped_ctx_push(context* c): c(c) { c->push(); } scoped_ctx_push(context* c): c(c) { c->push(); }
~scoped_ctx_push() { c->pop(1); } ~scoped_ctx_push() {
try {
c->pop(1);
}
catch (...) {
;
}
}
}; };
/** /**

23
src/smt/smt_parallel.cpp
View file

@ -193,14 +193,25 @@ namespace smt {
} }
catch (z3_error & err) { catch (z3_error & err) {
error_code = err.error_code(); if (finished_id == UINT_MAX) {
ex_kind = ERROR_EX; error_code = err.error_code();
done = true; ex_kind = ERROR_EX;
done = true;
}
} }
catch (z3_exception & ex) { catch (z3_exception & ex) {
ex_msg = ex.msg(); if (finished_id == UINT_MAX) {
ex_kind = DEFAULT_EX; ex_msg = ex.msg();
done = true; ex_kind = DEFAULT_EX;
done = true;
}
}
catch (...) {
if (finished_id == UINT_MAX) {
ex_msg = "unknown exception";
ex_kind = ERROR_EX;
done = true;
}
} }
}; };