From 684cb23b402b3de58b76141a690bb6f6219e99a4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 29 Mar 2026 19:30:13 -0700
Subject: [PATCH] turn on constraint integrity checking

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/seq/seq_nielsen.cpp |  9 ++-------
 src/smt/theory_nseq.cpp     | 12 ++++++++----
 2 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 417b0948b..f16c0a6df 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -287,7 +287,7 @@ namespace seq {
             expr* v = s.m_var->arg(0)->get_expr();
             expr* repl = s.m_replacement->arg(0)->get_expr();
             expr* eq = sg.get_manager().mk_eq(v, repl);
-            m_constraints.push_back(constraint(eq, s.m_dep, sg.get_manager()));
+            add_constraint(constraint(eq, s.m_dep, sg.get_manager()));
         }
     }
 
@@ -1496,12 +1496,7 @@ namespace seq {
         if (!node->is_extended()) {
             bool ext = generate_extensions(node);
             IF_VERBOSE(1, display(verbose_stream(), node));
-            if (!ext) {
-#ifdef Z3DEBUG
-                std::string dot = to_dot();
-                std::cout << dot << std::endl;
-#endif
-            }
+            CTRACE(seq, !ext, display(tout, node) << to_dot() << "\n");
             VERIFY(ext);
             node->set_extended(true);
             ++m_stats.m_num_extensions;
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 8617d3883..00a753cd8 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -90,7 +90,7 @@ namespace smt {
             if (is_not)
                 lit.neg();
             if (ctx.get_assignment(lit) == l_false) {
-                IF_VERBOSE(1, verbose_stream() << "literal_if_false: " << lit << " " << mk_pp(e, m) << " is assigned false\n");
+                TRACE(seq, tout << "literal_if_false: " << lit << " " << mk_pp(e, m) << " is assigned false\n");
                 return lit;
             }
             return sat::null_literal;
@@ -626,18 +626,20 @@ namespace smt {
 
 
     bool theory_nseq::add_nielsen_assumptions() {
-        return true;
+        // return true;
         bool has_undef = false;
         bool has_false = false;
         for (auto const& c : m_nielsen.sat_node()->constraints()) {
             auto lit = mk_literal(c.fml);
             switch (ctx.get_assignment(lit)) { 
-            case l_true: break;
+            case l_true: 
+                break;
             case l_undef:
                 has_undef = true; 
                 ctx.force_phase(lit);                
-                IF_VERBOSE(0, verbose_stream() << 
+                IF_VERBOSE(2, verbose_stream() << 
                     "nseq final_check: adding nielsen assumption " << c.fml << "\n";);
+                TRACE(seq, tout << "assign: " << c.fml << "\n");
                 break;
             case l_false: 
                 // do we really expect this to happen?
@@ -645,6 +647,8 @@ namespace smt {
                 IF_VERBOSE(0, verbose_stream()
                                   << "nseq final_check: nielsen assumption " << c.fml << " is false\n";);
                 ctx.force_phase(lit);
+                TRACE(seq, tout << "assigned to false: " << c.fml << "\n");
+                UNREACHABLE();
                 break;
             }
         }