mirror of
https://github.com/Z3Prover/z3
synced 2026-07-30 02:33:51 +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)). |
||
|---|---|---|
| .. | ||
| bounded model checking | ||
| complex | ||
| data | ||
| hamiltonian | ||
| mus | ||
| tutorial | ||
| all_interval_series.py | ||
| bincover.py | ||
| CMakeLists.txt | ||
| efsmt.py | ||
| example.py | ||
| hs.py | ||
| mini_ic3.py | ||
| mini_quip.py | ||
| parallel.py | ||
| prooflogs.py | ||
| proofreplay.py | ||
| rc2.py | ||
| README | ||
| simplify_formula.py | ||
| socrates.py | ||
| trafficjam.py | ||
| union_sort.py | ||
| visitor.py | ||
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.