From 008a101c08e188f6b4e32f94b6849fb56dff96af Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 1 Apr 2026 22:08:19 +0000
Subject: [PATCH] seq_eq_solver: add pointer-equality fast path in
 has_len_offset and use all_of in find_branch_candidate

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/73262603-7733-4009-b5c7-17e55c79fb85

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/seq_eq_solver.cpp | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index e368e137b..215447327 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -134,6 +134,11 @@ bool theory_seq::has_len_offset(expr_ref_vector const& ls, expr_ref_vector const
     if (!is_var(l_fst) || !is_var(r_fst)) 
         return false;
 
+    if (l_fst == r_fst) {
+        offset = 0;
+        return true;
+    }
+
     expr_ref len_l_fst = mk_len(l_fst);
     if (!ctx.e_internalized(len_l_fst)) 
         return false;
@@ -875,10 +880,7 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
         }
     }
 
-    bool all_units = true;
-    for (expr* r : rs) {
-        all_units &= m_util.str.is_unit(r);
-    }
+    bool all_units = all_of(rs, [&](auto* r) { return m_util.str.is_unit(r); });
     if (all_units) {
         literal_vector lits;
         lits.push_back(~mk_eq_empty(l));