From 168b63b44a287e6b8a9d9c1983d9eb80162b13ce Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 24 Apr 2026 01:59:48 +0000 Subject: [PATCH] Fix loop merging to use a->get_arg(0) consistently for body enode and expression Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/1b89b614-2acb-49ef-9603-df5dfa7a02af Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/euf/euf_seq_plugin.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/ast/euf/euf_seq_plugin.cpp b/src/ast/euf/euf_seq_plugin.cpp index a63de1b59..ae772478b 100644 --- a/src/ast/euf/euf_seq_plugin.cpp +++ b/src/ast/euf/euf_seq_plugin.cpp @@ -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); }