mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 03:16:21 +00:00
Code Activity

Fix loop merging to use a->get_arg(0) consistently for body enode and expression

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/1b89b614-2acb-49ef-9603-df5dfa7a02af

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-04-24 01:59:48 +00:00 • committed by GitHub
parent 218c55701d
commit 168b63b44a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/euf/euf_seq_plugin.cpp
View file

@ -269,11 +269,8 @@ namespace euf {
unsigned lo1, hi1, lo2, hi2;
if (same_loop_body(a, b, lo1, hi1, lo2, hi2)) {
ast_manager& m = g.get_manager();
expr* body_e = nullptr;
unsigned dummy_lo, dummy_hi;
m_seq.re.is_loop(a->get_expr(), body_e, dummy_lo, dummy_hi);
expr_ref merged(m_seq.re.mk_loop(body_e, lo1 + lo2, hi1 + hi2), m);
enode* body_n = a->get_arg(0);
expr_ref merged(m_seq.re.mk_loop(body_n->get_expr(), lo1 + lo2, hi1 + hi2), m);
enode* merged_n = mk(merged, 1, &body_n);
push_merge(n, merged_n);
}