From b095adfa815fd69e14195431b738b553a3901e96 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 3 Jul 2026 12:24:06 -0700
Subject: [PATCH] fixing unsoundness in concat rule

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_split.cpp | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp
index 92fa5f3747..63cad62564 100644
--- a/src/ast/rewriter/seq_split.cpp
+++ b/src/ast/rewriter/seq_split.cpp
@@ -36,7 +36,6 @@ struct split_set::imp {
         if (r) {
             VERIFY(seq.is_re(r, m_seq_sort));
             m_re_sort = r->get_sort();
-            TRACE(seq, tout << "split_set::imp: " << this << " " << mk_pp(r, m) << " threshold: " << m_threshold << "\n");
         }
         if (m_threshold == 0)
             m_threshold = UINT_MAX;
@@ -453,7 +452,6 @@ struct split_set::iterator::imp {
     }
 
     bool at_end() const {
-        TRACE(seq, tout << "split_set::iterator::at_end: " << this << " " << m_at_end << " " << m_qhead << "/" << m_splits.size() << "\n");
         return m_failure || (m_at_end && m_qhead == m_splits.size());
     }
 };