Fix nseq divergence: classify Skolem terms as s_var, fix at_axiom, remove UNREACHABLE, add stall detection, filter opaque equations, handle mk_seq_eq assignments

Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>

src/ast/euf/euf_sgraph.cpp

@@ -106,9 +106,9 @@ namespace euf {
         if (m_seq.str.is_in_re(e))
             return snode_kind::s_in_re;
 
-        // uninterpreted constants of string sort are variables
-        // NSB review: check is_uninterp instead of is_uninterp_const.
-        if (is_uninterp_const(e) && m_seq.is_seq(e->get_sort()))
+        // uninterpreted constants and Skolem string terms are variables
+        if (m_seq.is_seq(e->get_sort()) &&
+            (is_uninterp_const(e) || m_seq.is_skolem(e)))
             return snode_kind::s_var;
 
         return snode_kind::s_other;

src/ast/rewriter/seq_axioms.cpp

@@ -624,12 +624,13 @@ namespace seq {
             add_clause(~i_ge_0, i_ge_len_s, mk_seq_eq(nth, e));                
         }
         else {
-            expr_ref x =     m_sk.mk_pre(s, i);
-            expr_ref y =     m_sk.mk_tail(s, i);
-            expr_ref xey   = mk_concat(x, e, y);
-            expr_ref len_x = mk_len(x);
+            expr_ref x = m_sk.mk_pre(s, i);
+            expr_ref y = m_sk.mk_tail(s, i);
+            expr_ref nth(seq.str.mk_nth_i(s, i), m);
+            expr_ref unit_nth(seq.str.mk_unit(nth), m);
+            expr_ref xey = mk_concat(x, unit_nth, y);
             add_clause(~i_ge_0, i_ge_len_s, mk_seq_eq(s, xey));
-            add_clause(~i_ge_0, i_ge_len_s, mk_eq(i, len_x));
+            add_clause(~i_ge_0, i_ge_len_s, mk_eq(i, mk_len(x)));
         }
 
         add_clause(i_ge_0, mk_eq(e, emp));

src/smt/seq/seq_nielsen.cpp

@@ -2327,7 +2327,13 @@ namespace seq {
                     ++m_stats.m_num_unsat;
                     return r;
                 }
-                // depth limit hit – double the bound and retry
+                // depth limit hit – double the bound and retry, but only if the
+                // DFS actually reached the depth limit (max_depth >= depth_bound).
+                // If max_depth < depth_bound the bound was not the bottleneck
+                // (e.g. all nodes stalled on opaque terms or arithmetic), so
+                // doubling would not help and would cause an infinite loop.
+                if (m_stats.m_max_depth < m_depth_bound)
+                    break;
                 m_depth_bound *= 2;
                 SASSERT(m_depth_bound < INT_MAX);
             }
@@ -2428,7 +2434,6 @@ namespace seq {
         if (!node->is_extended()) {
             bool ext = generate_extensions(node);
             if (!ext) {
-                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

@@ -173,6 +173,19 @@ namespace smt {
         euf::snode* s1 = get_snode(e1);
         euf::snode* s2 = get_snode(e2);
         if (s1 && s2) {
+            // skip equations containing opaque (s_other) tokens; the Nielsen graph
+            // has no modifier to handle them and they only block extension generation
+            auto has_opaque = [](euf::snode* n) {
+                if (!n) return false;
+                if (n->kind() == euf::snode_kind::s_other) return true;
+                euf::snode_vector toks;
+                n->collect_tokens(toks);
+                for (auto* t : toks)
+                    if (t && t->kind() == euf::snode_kind::s_other) return true;
+                return false;
+            };
+            if (has_opaque(s1) || has_opaque(s2))
+                return;
             seq::dep_tracker dep = nullptr;
             ctx.push_trail(restore_vector(m_prop_queue));
             m_prop_queue.push_back(eq_item(s1, s2, get_enode(v1), get_enode(v2), dep));
@@ -248,7 +261,28 @@ namespace smt {
                  m_seq.str.is_is_digit(e) ||
                  m_seq.str.is_foldl(e) ||
                  m_seq.str.is_foldli(e)) {
-            // no-op: handled by other mechanisms
+            // when the special seq-equality Skolem is assigned true, add the word equation
+            expr* lhs = nullptr, *rhs = nullptr;
+            if (is_true && m_axioms.sk().is_eq(e, lhs, rhs) &&
+                m_seq.is_seq(lhs) && m_seq.is_seq(rhs)) {
+                euf::snode* s1 = get_snode(lhs);
+                euf::snode* s2 = get_snode(rhs);
+                auto has_opaque = [](euf::snode* n) {
+                    if (!n) return false;
+                    if (n->kind() == euf::snode_kind::s_other) return true;
+                    euf::snode_vector toks;
+                    n->collect_tokens(toks);
+                    for (auto* t : toks)
+                        if (t && t->kind() == euf::snode_kind::s_other) return true;
+                    return false;
+                };
+                if (s1 && s2 && !has_opaque(s1) && !has_opaque(s2)) {
+                    seq::dep_tracker dep = nullptr;
+                    ctx.push_trail(restore_vector(m_prop_queue));
+                    m_prop_queue.push_back(eq_item(s1, s2, nullptr, nullptr, dep));
+                }
+            }
+            // no-op for other Skolems: handled by other mechanisms
         }
         else if (is_app(e) && to_app(e)->get_family_id() == m_seq.get_family_id())
             push_unhandled_pred();