From 598e4ede4e33a23f5ef9eca6d29bd9527d793463 Mon Sep 17 00:00:00 2001
From: CEisenhofer <clemens.eisenhofer@tuwien.ac.at>
Date: Thu, 9 Apr 2026 11:03:18 +0200
Subject: [PATCH] Removed debug code

---
 src/smt/seq/seq_nielsen.cpp | 5 +----
 src/smt/theory_nseq.cpp     | 2 +-
 2 files changed, 2 insertions(+), 5 deletions(-)

diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 923a530a9..6a1aef508 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -264,10 +264,8 @@ namespace seq {
         m_constraints.push_back(c);
         SASSERT(m_graph.m_literal_if_false);
         auto lit = m_graph.m_literal_if_false(c.fml);
-        if (lit != sat::null_literal) {
-            std::cout << "External literal " << lit << " in node " << m_id << std::endl;
+        if (lit != sat::null_literal)
             set_external_conflict(lit, c.dep);
-        }
     }
 
     void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) {
@@ -3704,7 +3702,6 @@ namespace seq {
             if (n->m_conflict_external_literal != sat::null_literal) {
                 // We know from the outer solver that this literal is assigned false
                 deps = m_dep_mgr.mk_join(deps, m_dep_mgr.mk_leaf(n->m_conflict_external_literal));
-                std::cout << "External literal: " << n->m_conflict_external_literal << std::endl;
                 if (n->m_conflict_internal)
                     deps = m_dep_mgr.mk_join(deps, n->m_conflict_internal);
                 continue;
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 22aaead53..23fdbcd19 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -734,7 +734,7 @@ namespace smt {
         set_conflict(eqs, lits);
 
 #ifdef Z3DEBUG
-#if 1
+#if 0
         // Pass constraints to a subsolver to check correctness modulo legacy solver
         {
             smt_params p;