mirror of
https://github.com/Z3Prover/z3
synced 2026-06-19 15:16:29 +00:00
c67bb140dc
## Summary egex_bisim::collect_leaves used to descend through `re.union` and `re.antimirov_union` at the top of each leaf of the transition regex, splitting a single bisimulation state into multiple states before they were merged into the union-find. This contradicts the bisimulation invariant: **each leaf of a t-regex represents one state, regardless of its top-level shape**. The fix descends into `ite` only (which is the actual structural splitter of guarded transitions). ## Why it matters The split happens to be *sound* for the current algorithm when the goal is asserting `L(union(A, B)) = empty` (since `L(A) = empty AND L(B) = empty` is equivalent), but it: 1. Adds spurious merges to the union-find that distort state-class identities. 2. Slows convergence on hard equivalence queries (and causes early timeouts in practice). 3. Creates latent unsoundness risk for any extension that interprets leaves more semantically (XOR pair handling, classical-flag propagation, future antimirov re-enable, etc.). ## Empirical validation Run on the 1523-file regex-equivalence corpus, 5s/file timeout, 8 workers: | metric | pre-fix master | post-fix | |---|---|---| | sat | 1008 | 1014 | | unsat | 368 | 368 | | timeout | 145 | 139 | | unknown | 2 | 2 | | SAT↔UNSAT verdict flips | — | **0** | | timeout→sat flips | — | 6 | | commonly-solved wall ratio | 1.000x | **0.902x** | The 6 `timeout` → `sat` cases all return the *same* `sat` under pre-fix master if given 60s; they are previously-slow cases not previously-wrong ones. Z3 unit tests: 89/89 pass (`test-z3 /a`). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> |
||
|---|---|---|
| .. | ||
| ackermannization | ||
| api | ||
| ast | ||
| cmd_context | ||
| math | ||
| model | ||
| muz | ||
| nlsat | ||
| opt | ||
| params | ||
| parsers | ||
| qe | ||
| sat | ||
| shell | ||
| smt | ||
| solver | ||
| tactic | ||
| test | ||
| util | ||
| CMakeLists.txt | ||