mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-17 18:43:45 +00:00
Code Activity

Address code review feedback: improve null-sort handling in seq_model and some_seq_in_re

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-14 23:17:32 +00:00
parent fdec148903
commit 891b2e6c8e
2 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/rewriter/seq_rewriter.cpp
View file

@ -6016,7 +6016,9 @@ void seq_rewriter::op_cache::cleanup() {
lbool seq_rewriter::some_seq_in_re(expr* r, expr_ref& result) {
sort* seq_sort = nullptr;
if (u().is_re(r, seq_sort) && u().is_string(seq_sort)) {
if (!u().is_re(r, seq_sort))
return l_undef;
if (u().is_string(seq_sort)) {
zstring s;
lbool res = some_string_in_re(r, s);
if (res == l_true)
@ -6024,9 +6026,10 @@ lbool seq_rewriter::some_seq_in_re(expr* r, expr_ref& result) {
return res;
}
// For non-string sequences: check if the regex accepts the empty sequence.
SASSERT(seq_sort);
expr_ref is_null = is_nullable(r);
if (m().is_true(is_null)) {
result = str().mk_empty(seq_sort ? seq_sort : str().mk_string_sort());
result = str().mk_empty(seq_sort);
return l_true;
}
return l_undef;

1
src/smt/seq_model.cpp
View file

@ -233,6 +233,7 @@ namespace smt {
// Build the repeated string: base^exp_val
if (exp_val.is_zero()) {
sort* srt = n->get_sort();
SASSERT(srt);
if (!srt) srt = m_seq.str.mk_string_sort();
return expr_ref(m_seq.str.mk_empty(srt), m);
}