diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index dd07362b6..5dae6921d 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3094,15 +3094,8 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { bool seq_rewriter::has_fixed_length_constraint(expr* a, unsigned& len) { unsigned minl = re().min_length(a), maxl = re().max_length(a); - if (minl == maxl) { - len = minl; - return true; - } - expr* b = nullptr, *c = nullptr; - if (re().is_intersection(a, b, c)) { - return has_fixed_length_constraint(b, len) || has_fixed_length_constraint(c, len); - } - return false; + len = minl; + return minl == maxl; } br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {