mirror of
https://github.com/Z3Prover/z3
synced 2026-06-19 15:16:29 +00:00
0b8bb98656
`seq::derive::operator()(ele, r)` looks up `m_top_cache` keyed only by the regex `r`, but on a miss it used to set `m_ele = ele` (a concrete char) before calling `derive_rec(r)`. The resulting ITE-tree contained constant-folded `(= ele c)` conditions, so the "symbolic" derivative stored in the cache was actually specialized to that one ele. Subsequent calls with the same `r` but a different ele hit the stale cached answer and the substitution at the bottom was a no-op (no `v0` left to replace). Simplest victim: (str.in_re "aP" (re.++ (re.* "a") "P")) returned `unsat`. The first call D_'a'(a*P) computed `a*P` and cached it under key `a*P`; the next call D_'P'(a*P) hit that cache entry and returned `a*P` instead of epsilon, so the membership check ended on a non-nullable state. Fix: set `m_ele = v` (the canonical fresh var) so the derivative is genuinely symbolic. Concrete-ele callers go through the existing substitution at the bottom of `operator()`. Adds a regression test in src/test/seq_regex_bisim.cpp checking that D_'a'(a*P) is not nullable while D_'P'(a*P) is. Note: this is independent of the mut_0013 bisim-level unsoundness; that case still fails and is being tracked separately. 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 | ||