mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

vurtego update

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-13 19:46:12 -07:00
parent a56c9faedb
commit 732a8149d8
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/qe/qe_mbi.cpp
View file

@ -479,8 +479,11 @@ namespace qe {
else if !is_sat(local & lits) then
return l_false, mbp of local, nullptr
else if is_sat(local & lits) && !is_sat(local & lits & blocked)
MISSING CASE. IS IT POSSIBLE?
MISSING CASE
MUST PRODUCE AN IMPLICANT OF LOCAL that is inconsistent with lits & blocked
in this case !is_sat(local & lits & mdl) so
return l_false, core of lits & mdl, nullptr
this will force a new mdl
mbi_plugin::block(phi): add phi to blocked