From 732a8149d8b3662e6482f3070319c1de40120b12 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Wed, 13 Jun 2018 19:46:12 -0700
Subject: [PATCH] vurtego update

---
 src/qe/qe_mbi.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
index 57dfff941..6f2c346f0 100644
--- a/src/qe/qe_mbi.cpp
+++ b/src/qe/qe_mbi.cpp
@@ -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