mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

Hoist seq length rewrite out of loop

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-07-13 20:23:15 +00:00 • committed by GitHub
parent 026971075b
commit c75a034739
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_seq.cpp
View file

@ -1013,9 +1013,9 @@ bool theory_seq::add_solution(expr* l, expr* r, dependency* deps) {
tout << "#" << n1->get_owner_id() << " ==> #" << n2->get_owner_id() << "\n"; tout << "#" << n1->get_owner_id() << " ==> #" << n2->get_owner_id() << "\n";
tout << (n1->get_root() == n2->get_root()) << "\n";); tout << (n1->get_root() == n2->get_root()) << "\n";);
propagate_eq(deps, n1, n2); propagate_eq(deps, n1, n2);
expr_ref len_r(m_util.str.mk_length(r), m);
m_rewrite(len_r);
for (expr* len_e : len_parents) { for (expr* len_e : len_parents) {
expr_ref len_r(m_util.str.mk_length(r), m);
m_rewrite(len_r);
propagate_eq(deps, len_e, len_r, false); propagate_eq(deps, len_e, len_r, false);
} }
return true; return true;