mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-04 22:36:10 +00:00
Code Activity

bugfix for empty ranges

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-03 13:34:37 -07:00
parent b2ccb2552f
commit a07b71cabe
1 changed files with 0 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -4155,10 +4155,6 @@ 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;
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