From a07b71cabe42137e93d40937c09a4410d970ab58 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2026 13:34:37 -0700 Subject: [PATCH] bugfix for empty ranges Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index d1df4133b1..5de672b1a2 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -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