From 206569c0d68ea938e851be0cbfc64913d3a606f2 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Sat, 6 Jun 2026 13:25:16 -0700
Subject: [PATCH] fix: negate offset on swap in seq_offset_eq::find (#9722)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`seq_offset_eq::find` returned the stored offset with the wrong sign
whenever the enode arguments were reordered to match the canonical key
ordering (`r1.id ≤ r2.id`), causing `len_based_split` to silently skip
~50% of eligible length-based splits.

### Root cause

`m_offset_equalities` stores `(rA, rB) → v` meaning `len(rA) − len(rB) =
v` with `rA.id ≤ rB.id`. `len_offset()` correctly negates `val` when
inserting with swapped keys. `find()` performed the same swap for the
lookup but never negated the returned value, so callers received
`len(n2) − len(n1)` instead of `len(n1) − len(n2)`.

### Fix

```cpp
// BEFORE
if (n1->get_owner_id() > n2->get_owner_id())
    std::swap(n1, n2);
if (m_offset_equalities.find(n1, n2, offset))
    return offset;  // wrong sign when swapped

// AFTER
bool swapped = n1->get_owner_id() > n2->get_owner_id();
if (swapped)
    std::swap(n1, n2);
if (m_offset_equalities.find(n1, n2, offset))
    return swapped ? -offset : offset;
```

This makes `find` consistent with the documented contract (`r1 = r2 +
offset`) and symmetric with the insertion logic in `len_offset()`.

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 src/smt/seq_offset_eq.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/smt/seq_offset_eq.cpp b/src/smt/seq_offset_eq.cpp
index 2bc933bcd..f9c7adafc 100644
--- a/src/smt/seq_offset_eq.cpp
+++ b/src/smt/seq_offset_eq.cpp
@@ -97,13 +97,14 @@ void seq_offset_eq::prop_arith_to_len_offset() {
 std::optional<int> seq_offset_eq::find(enode* n1, enode* n2) const {
     n1 = n1->get_root();
     n2 = n2->get_root();
-    if (n1->get_owner_id() > n2->get_owner_id()) 
+    bool swapped = n1->get_owner_id() > n2->get_owner_id();
+    if (swapped)
         std::swap(n1, n2);
     if (a.is_numeral(n1->get_expr()) || a.is_numeral(n2->get_expr()))
         return std::nullopt;
     int offset;
     if (m_offset_equalities.find(n1, n2, offset))
-        return offset;
+        return swapped ? -offset : offset;
     return std::nullopt;
 }