mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-08 23:11:20 +00:00
Code Activity

Fix regex ITE propagation (#10379) (#10431)

Browse source 
Preserve both regex membership branches while an ITE condition is
unresolved so the selected branch is enforced after assignment.

fix #10379 

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Copilot-Session: a8f87ede-b718-4fe9-9839-cc9eaaf9c3a7
This commit is contained in:
Nikolaj Bjorner 2026-08-06 21:39:20 -07:00 • committed by GitHub
parent 991d4be5f1
commit 2c508b3753
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 26 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/seq_regex.cpp
View file

@ -568,6 +568,12 @@ namespace smt {
}
case l_undef: {
ctx.mark_as_relevant(c_lit);
// The membership literal is asserted only once, so preserve both
// branches until the condition receives an assignment.
literal in_t = th.mk_literal(re().mk_in_re(s, t));
literal in_e = th.mk_literal(re().mk_in_re(s, e));
th.add_axiom(~lit, ~c_lit, in_t);
th.add_axiom(~lit, c_lit, in_e);
break;
}
}

20
src/test/seq_monadic.cpp
View file

@ -674,6 +674,26 @@ public:
check_smt("enabled SAT membership", assertions, l_true);
check_smt("disabled legacy membership", assertions, l_true, false);
}
{
arith_util ar2(m);
expr_ref zero(ar2.mk_int(0), m);
expr_ref one(ar2.mk_int(1), m);
expr_ref k = var("issue_10379_k");
expr_ref k0(u.str.mk_at(k, zero), m);
expr_ref mod00(ar2.mk_mod(zero, zero), m);
expr_ref inner_cond(re().mk_in_re(sword("1"), re().mk_to_re(k)), m);
expr_ref inner(m.mk_ite(
inner_cond,
sconcat(sword("n"), k0),
u.str.mk_substr(k, zero, mod00)), m);
expr_ref outer_regex(cat(re().mk_to_re(k0), rng('a', 'z')), m);
expr_ref outer_cond(re().mk_in_re(inner, outer_regex), m);
expr_ref rhs(m.mk_ite(outer_cond, k0, u.str.mk_substr(k, zero, zero)), m);
expr_ref_vector assertions(m);
assertions.push_back(m.mk_eq(k, rhs));
assertions.push_back(ar2.mk_ge(u.str.mk_length(k), one));
check_smt("legacy nested regex ITE issue 10379", assertions, l_false, false);
}
{
expr_ref_vector assertions(m);
expr_ref a_star(star(a), m);