mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

check result of unsat core validation

Browse source
This commit is contained in:
Murphy Berzish 2017-04-22 13:36:09 -04:00
parent a1bb1f2a13
commit 367cc4b77f
1 changed files with 12 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/smt/smt_context.cpp
View file

@ -3281,13 +3281,21 @@ namespace smt {
TRACE("after_internalization", display(tout);); TRACE("after_internalization", display(tout););
if (inconsistent()) { if (inconsistent()) {
VERIFY(!resolve_conflict()); // build the proof VERIFY(!resolve_conflict()); // build the proof
mk_unsat_core(); lbool result = mk_unsat_core();
r = l_false; if (result == l_undef) {
r = l_undef;
} else {
r = l_false;
}
} }
else { else {
r = search(); r = search();
if (r == l_false) if (r == l_false) {
mk_unsat_core(); lbool result = mk_unsat_core();
if (result == l_undef) {
r = l_undef;
}
}
} }
} }
} }