From 8bbac04a266c4798185b2a44029f7a542973906b Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 28 Apr 2026 16:12:33 +0000 Subject: [PATCH] Refactor: extract saturating_add helper, simplify hash-check condition Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/da8647c4-ddff-47ce-9364-2eee3810c38d Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/euf/euf_seq_plugin.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/ast/euf/euf_seq_plugin.cpp b/src/ast/euf/euf_seq_plugin.cpp index d1c08c7ba..dcbea9883 100644 --- a/src/ast/euf/euf_seq_plugin.cpp +++ b/src/ast/euf/euf_seq_plugin.cpp @@ -46,6 +46,11 @@ namespace euf { } } + // Saturating unsigned addition: returns UINT_MAX instead of wrapping. + static unsigned saturating_add(unsigned a, unsigned b) { + return (b > UINT_MAX - a) ? UINT_MAX : a + b; + } + unsigned enode_concat_hash::operator()(enode* n) const { snode* sn = sg.find(n->get_expr()); if (sn && sn->has_cached_hash()) @@ -70,8 +75,8 @@ namespace euf { if (sa && sb && sa->length() != sb->length()) return false; // fast-path: cached associativity hash (O(1)) - if (sa && sa->has_cached_hash() && sb && sb->has_cached_hash() && - sa->assoc_hash() != sb->assoc_hash()) + bool both_have_hash = sa && sa->has_cached_hash() && sb && sb->has_cached_hash(); + if (both_have_hash && sa->assoc_hash() != sb->assoc_hash()) return false; enode_vector la, lb; collect_enode_leaves(a, seq, la); @@ -264,8 +269,8 @@ namespace euf { ast_manager& m = g.get_manager(); enode* body_n = a->get_arg(0); // saturating add: prevent silent unsigned wrap-around on large bounds - unsigned lo_merged = (lo2 > UINT_MAX - lo1) ? UINT_MAX : lo1 + lo2; - unsigned hi_merged = (hi2 > UINT_MAX - hi1) ? UINT_MAX : hi1 + hi2; + unsigned lo_merged = saturating_add(lo1, lo2); + unsigned hi_merged = saturating_add(hi1, hi2); expr_ref merged(m_seq.re.mk_loop(body_n->get_expr(), lo_merged, hi_merged), m); enode* merged_n = mk(merged, 1, &body_n); push_merge(n, merged_n);