From 0e9fd52af4fe376aef0adfe3c05063544b9eb877 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Sun, 5 Jul 2026 00:13:07 -0700 Subject: [PATCH] seq: fix re.range with empty-string bound wrongly left symbolic 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> --- src/ast/rewriter/seq_rewriter.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 5de672b1a2..79c542f06b 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -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