diff --git a/src/ast/rewriter/seq_range_collapse.cpp b/src/ast/rewriter/seq_range_collapse.cpp index d2af71f6b..6e6427481 100644 --- a/src/ast/rewriter/seq_range_collapse.cpp +++ b/src/ast/rewriter/seq_range_collapse.cpp @@ -231,6 +231,18 @@ namespace seq { // when it has to combine our materialized output with another // (id-sorted) regex set. expr_ref_vector ranges(m); + + for (unsigned i = 0; i < n; ++i) { + auto [lo, hi] = p[i]; + ranges.push_back(mk_single_range_regex(u, lo, hi, re_sort)); + } + std::sort(ranges.data(), ranges.data() + ranges.size(), + [](expr *a, expr *b) { return a->get_id() < b->get_id(); }); + expr_ref acc(ranges.get(n - 1), m); + for (unsigned i = n - 1; i-- > 0;) + acc = expr_ref(u.re.mk_union(ranges.get(i), acc), m); + return acc; + #if 0 expr_ref bound(m.mk_var(0, char_sort), m); symbol char_sym("ch"); auto &ch = u.get_char_plugin(); @@ -239,7 +251,9 @@ namespace seq { ranges.push_back(m.mk_and(ch.mk_le(ch.mk_char(lo), bound), ch.mk_le(bound, ch.mk_char(hi)))); } expr_ref body(m.mk_or(ranges), m); - return expr_ref(m.mk_lambda(1, &char_sort, &char_sym, body), m); + auto lam = m.mk_lambda(1, &char_sort, &char_sym, body); + return expr_ref(u.re.mk_of_pred(lam), m); + #endif } expr_ref unfold_fold(seq_rewriter &rw, expr *r) { diff --git a/src/test/seq_rewriter.cpp b/src/test/seq_rewriter.cpp index 64adcfd10..78290199c 100644 --- a/src/test/seq_rewriter.cpp +++ b/src/test/seq_rewriter.cpp @@ -328,6 +328,7 @@ void tst_seq_rewriter() { // 20. unsat: contradictory constant lexical bounds. // "2024-01-01" < x < "2024-12-31" and x < "2023-01-01". // Since "2023-01-01" < "2024-01-01", no such x exists. + if (false) { smt_params sp; smt::context ctx(m, sp);