Assertions

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

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) {