From ec495c094c15f5ef41976cef7af1c1a44a123b61 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 1 Apr 2026 22:06:52 +0000
Subject: [PATCH] seq_ne_solver: short-circuit propagate_ne2eq for str.unit
 elements

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/269206ba-eec0-4986-93b3-738478e88991

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/seq_ne_solver.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/smt/seq_ne_solver.cpp b/src/smt/seq_ne_solver.cpp
index 5abed268c..263c94212 100644
--- a/src/smt/seq_ne_solver.cpp
+++ b/src/smt/seq_ne_solver.cpp
@@ -134,11 +134,12 @@ bool theory_seq::propagate_ne2eq(unsigned idx, expr_ref_vector const& es) {
     if (es.empty())
         return false;
     for (expr* e : es) {
+        if (m_util.str.is_unit(e))
+            return true;
         expr_ref len_e = mk_len(e);
         rational lo;
-        if (lower_bound(len_e, lo) && lo > 0) {
+        if (lower_bound(len_e, lo) && lo > 0)
             return true;
-        }
     }
     ne const& n = m_nqs[idx];
     expr_ref e(m), head(m), tail(m);