From 2a5bfb818b302a3a231152d10c2bf1e1370c0ab7 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Fri, 23 Jan 2026 10:18:51 -0800
Subject: [PATCH] Refactor seq_offset_eq::find to use std::optional (#8300)

* Initial plan

* Refactor seq_offset_eq::find to use std::optional

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/seq_eq_solver.cpp |  3 ++-
 src/smt/seq_offset_eq.cpp | 12 +++++++-----
 src/smt/seq_offset_eq.h   |  6 ++++--
 3 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index f8cb8586e..f91cb80d3 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -150,7 +150,8 @@ bool theory_seq::has_len_offset(expr_ref_vector const& ls, expr_ref_vector const
         return true;
     }
 
-    if (m_offset_eq.find(root1, root2, offset)) {
+    if (auto opt_offset = m_offset_eq.find(root1, root2)) {
+        offset = *opt_offset;
         TRACE(seq, tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << " " << offset << ")\n";);
         return true;
     }
diff --git a/src/smt/seq_offset_eq.cpp b/src/smt/seq_offset_eq.cpp
index 893c455d9..2bc933bcd 100644
--- a/src/smt/seq_offset_eq.cpp
+++ b/src/smt/seq_offset_eq.cpp
@@ -94,15 +94,17 @@ void seq_offset_eq::prop_arith_to_len_offset() {
     }
 }
 
-bool seq_offset_eq::find(enode* n1, enode* n2, int& offset) const {
+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()) 
         std::swap(n1, n2);
-    return 
-        !a.is_numeral(n1->get_expr()) && 
-        !a.is_numeral(n2->get_expr()) && 
-        m_offset_equalities.find(n1, n2, offset);
+    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 std::nullopt;
 }
 
 bool seq_offset_eq::contains(enode* r) {
diff --git a/src/smt/seq_offset_eq.h b/src/smt/seq_offset_eq.h
index 3535343fd..669d63b7f 100644
--- a/src/smt/seq_offset_eq.h
+++ b/src/smt/seq_offset_eq.h
@@ -21,6 +21,7 @@ Author:
 #include "ast/seq_decl_plugin.h"
 #include "ast/arith_decl_plugin.h"
 #include "smt/smt_theory.h"
+#include <optional>
 
 namespace smt {
 
@@ -43,9 +44,10 @@ namespace smt {
         bool empty() const { return m_offset_equalities.empty(); }
         /**
            \brief determine if r1 = r2 + offset
+           \return optional containing the offset if found, nullopt otherwise
          */
-        bool find(enode* r1, enode* r2, int& offset) const;
-        bool contains(enode* r1, enode* r2) const { int offset = 0; return find(r1, r2, offset); }
+        std::optional<int> find(enode* r1, enode* r2) const;
+        bool contains(enode* r1, enode* r2) const { return find(r1, r2).has_value(); }
         bool contains(enode* r);
         bool propagate();
         void pop_scope_eh(unsigned num_scopes);