mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

disable loop split set

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-05 12:03:27 -07:00
parent 3f62cb9932
commit 6610545c08
2 changed files with 2 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/seq_split.cpp
View file

@ -458,7 +458,7 @@ struct split_set::iterator::imp {
// where r{lo_i,hi_i} folds the tail counts j-i-1, over every remaining
// j in [l,h] with j > i, into a single loop [<eps,eps> when l == 0]
unsigned l, h;
if (re.is_loop(r, a, l, h)) {
if (false && re.is_loop(r, a, l, h)) {
if (l == 0) {
auto eps = mk_eps();
push_split(eps, eps);

5
src/smt/seq_regex.cpp
View file

@ -444,8 +444,6 @@ namespace smt {
// Final check also unfolds this axiomatization
// (we have to add a final check to seq_regex for this).
unsigned threshold = th.get_fparams().m_seq_regex_factorization_threshold;
expr_ref_vector prefix(m);
expr *hd, *tl, *v;
@ -477,8 +475,7 @@ namespace smt {
}
if (!result.failed()) {
const expr_ref cases_expr(m.mk_or(cases), m);
ctx.internalize(cases_expr, false);
th.propagate_lit(nullptr, 1, &lit, ctx.get_literal(cases_expr));
th.propagate_lit(nullptr, 1, &lit, th.mk_literal(cases_expr));
return true;
}
}