mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Make sure init is included when generalize

Browse source
This commit is contained in:
Huanyi Chen 2018-12-28 12:42:28 -05:00
parent b083c7546e
commit 300e99b67a
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
examples/python/mini_ic3.py
View file

@ -331,7 +331,9 @@ class MiniIC3:
def generalize(self, cube, f): def generalize(self, cube, f):
s = self.states[f - 1].solver s = self.states[f - 1].solver
if unsat == s.check(cube): 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 return cube, f
# Check if the negation of cube is inductive at level f # Check if the negation of cube is inductive at level f