From 2bd5283f6a9f089f335487cbc6a077037468744d Mon Sep 17 00:00:00 2001
From: CEisenhofer <clemens.eisenhofer@tuwien.ac.at>
Date: Fri, 20 Mar 2026 15:11:51 +0100
Subject: [PATCH] Assertions

---
 src/smt/seq/seq_nielsen.cpp | 3 ++-
 src/smt/theory_nseq.cpp     | 4 ++++
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 19d3c6f76..56a011c71 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -2329,6 +2329,7 @@ namespace seq {
                 }
                 // depth limit hit – double the bound and retry
                 m_depth_bound *= 2;
+                SASSERT(m_depth_bound < INT_MAX);
             }
             ++m_stats.m_num_unknown;
             return search_result::unknown;
@@ -2427,7 +2428,7 @@ namespace seq {
         if (!node->is_extended()) {
             bool ext = generate_extensions(node);
             if (!ext) {
-                node->set_extended(true);
+                UNREACHABLE();
                 // No extensions could be generated. If the node still has
                 // unsatisfied constraints with opaque (s_other) terms that
                 // we cannot decompose, report unknown rather than unsat
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 9e1149984..b1854be09 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -294,6 +294,9 @@ namespace smt {
                 propagate_pos_mem(std::get<mem_item>(item));
             else if (std::holds_alternative<axiom_item>(item))
                 dequeue_axiom(std::get<axiom_item>(item).e);
+            else {
+                UNREACHABLE();
+            }
         }
     }
 
@@ -537,6 +540,7 @@ namespace smt {
         // Examining the Nielsen graph is probably the best way of debugging
         std::string dot = m_nielsen.to_dot();
         IF_VERBOSE(1, verbose_stream() << dot << "\n";);
+        // std::cout << "Got: " << (result == seq::nielsen_graph::search_result::sat ? "sat" : (result == seq::nielsen_graph::search_result::unsat ? "unsat" : "unknown")) << std::endl;
 #endif
 
         if (result == seq::nielsen_graph::search_result::unsat) {