mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-27 09:22:41 +00:00
Code Activity

seq: fix re.range with empty-string bound wrongly left symbolic

Browse source 
The "Derive with ranges" refactor (#9963/#9965) dropped mk_re_range's
emptiness detection for a bound that is provably the empty string. Only
min_length > 1 was kept, which misses a length-0 bound: (re.range "" X)
was left as BR_FAILED (symbolic) instead of being simplified to the empty
regex. The derivative engine then produces a stuck derivative for such a
range and the theory can no longer decide membership, so benchmarks like
iss-5134/small.smt2 regressed from sat (model a="a") to unknown with
'model is not available'.

Restore the sound emptiness check: a bound whose max_length is provably 0
can never be a single character, so the range is empty. max_length == 0 is
a provable fact and is never true for a model-dependent (symbolic) bound,
so this does not reintroduce the unsoundness the refactor guarded against
(e.g. (re.range x x) is still left symbolic).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-07-05 00:13:07 -07:00 • committed by GitHub
parent 557a0cadab
commit 0e9fd52af4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/rewriter/seq_rewriter.cpp
View file

@ -4155,6 +4155,14 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
len = min_length(hi).second;
if (len > 1)
is_empty = true;
// A bound that is provably of length 0 (e.g. the empty string "") can
// likewise never be a single character, so the range is empty. Unlike a
// symbolic bound, max_length == 0 is a provable emptiness fact, so this is
// sound (it is never true for a model-dependent bound such as a variable).
if (max_length(lo) == std::make_pair(true, rational(0)))
is_empty = true;
if (max_length(hi) == std::make_pair(true, rational(0)))
is_empty = true;
// A provable length constraint (a bound can never be a single character)
// is the only sound way to conclude emptiness for a possibly-symbolic