From a4cfbfa274ff21c669ee744b060aeec4715edf3b Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 3 Apr 2026 02:12:35 +0000
Subject: [PATCH] Add clarifying comment to m_str_eq.empty() postcondition

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/24442582-8437-45ae-a58f-957ac2bdf698

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

diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index b39c6e7e9..c213bb4df 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -1207,6 +1207,8 @@ namespace seq {
 
 
         if (is_satisfied()) {
+            // pass 1 removed all trivial str_eq entries; is_satisfied() requires
+            // the remainder to be trivial, so the vector must be empty here.
             SASSERT(m_str_eq.empty());
             return simplify_result::satisfied;
         }