From 300e99b67ad07757b7d8820770157b8ded12cb9b Mon Sep 17 00:00:00 2001
From: Huanyi Chen <huanyi-chen@hotmail.com>
Date: Fri, 28 Dec 2018 12:42:28 -0500
Subject: [PATCH] Make sure init is included when generalize

---
 examples/python/mini_ic3.py | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/examples/python/mini_ic3.py b/examples/python/mini_ic3.py
index a509d6ff8..a62df48da 100644
--- a/examples/python/mini_ic3.py
+++ b/examples/python/mini_ic3.py
@@ -331,7 +331,9 @@ class MiniIC3:
     def generalize(self, cube, f):
         s = self.states[f - 1].solver
         if unsat == s.check(cube):
-            return s.unsat_core(), f
+            core = s.unsat_core()
+            if not check_disjoint(self.init, self.prev(And(core))):
+                return core, f
         return cube, f
 
     # Check if the negation of cube is inductive at level f