mirror of
https://github.com/Z3Prover/z3
synced 2026-04-15 08:44:10 +00:00
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)). |
||
|---|---|---|
| .. | ||
| c | ||
| c++ | ||
| dotnet | ||
| go | ||
| java | ||
| maxsat | ||
| ml | ||
| python | ||
| SMT-LIB2/bounded model checking | ||
| tptp | ||
| userPropagator | ||
| CMakeLists.txt | ||