mirror of
https://github.com/Z3Prover/z3
synced 2026-06-08 12:59:34 +00:00
Guangyu (Gary) HU
704dc9375d
Two fixes in examples/python/mini_ic3.py: 1. generalize(): the polarity of the disjointness check was inverted, and there was no guard against an empty unsat core. With an empty core, And([])=True so check_disjoint(init, prev(True)) is always False (init is sat), and the code returned the empty core. That empty core then became cube2clause([])=Or([])=False, which got added as a lemma to all frames. The frame became inconsistent and is_valid() returned And(Or())=False as the "inductive invariant". Fix: require len(core) > 0 AND check_disjoint(init, prev(core)) (without the spurious 'not'), so the core is only used when it is genuinely disjoint from init. 2. is_transition(): when an init rule's body happens to be an And without any Invariant predicate (e.g. (and (not A) (not B) ...)), is_body() returns (And(...), None). is_transition then passed inv0=None to subst_vars() which crashed inside get_vars(). Add an explicit None check so the rule falls through to is_init(). Verified on horn1..5 (unchanged behavior), h_CRC and h_FIFO from the blocksys benchmarks (now correctly return CEX matching z3 spacer), and cache_coherence_three (no longer collapses to (and or)).
The example is copied to the build directory during configuration.
You can execute it using
python example.py
in the build directory after you build Z3.