We need a better witness during model construction

src/smt/seq_model.cpp

@@ -122,11 +122,26 @@ namespace smt {
             return alloc(expr_wrapper_proc, e);
         }
 
-        // For nth_u (underspecified nth), return a fresh value of the element sort.
+        // For nth_u (underspecified nth): the Nielsen character-peel /
-        // NSB review: this looks plain wrong.
+        // regex-if-split records the chosen character as a relevant
+        // equality literal (e.g. (= (seq.nth_u x 0) (_ Char 65))), so the
+        // enode's equivalence class contains the required character
+        // constant. Use it; only fall back to a fresh value when the
+        // peeled character is genuinely unconstrained.
         if (m_seq.str.is_nth_u(e)) {
             sort *srt = e->get_sort();
-            expr *val = m_factory->get_fresh_value(srt);
+            expr* val = nullptr;
+            enode* it = n;
+            do {
+                if (m.is_value(it->get_expr())) {
+                    val = it->get_expr();
+                    break;
+                }
+                it = it->get_next();
+            }
+            while (it != n);
+            if (!val)
+                val = m_factory->get_fresh_value(srt);
             if (val) {
                 m_trail.push_back(val);
                 return alloc(expr_wrapper_proc, to_app(val));
@@ -258,13 +273,12 @@ namespace smt {
         // the exact traversal order of collect_dependencies so that the `values`
         // vector (model values for enode dependencies) is consumed consistently.
         //
-        // Computed nodes (concat / power / variable) are memoized in node2value
+        // Computed nodes (concat / power / variable) are memorized in node2value
         // keyed by (snode id, is_recursive). The recursion flag is part of the
         // key because the SAME variable snode appears in two distinct roles in a
         // Nielsen substitution such as D -> "cc" D: the outer variable being
         // defined (is_recursive == false, value == value of its replacement) and
-        // the inner "leftover" remainder (is_recursive == true, value == ""). A
+        // the inner "leftover" remainder (is_recursive == true, value == "").
-        // single id-keyed map would let the leftover clobber the outer value.
         uint_set seen;
         u_map<expr *> var2value;
         u_map<expr *> node2value;
@@ -381,12 +395,17 @@ namespace smt {
                     val = rv;
                 }
                 else if (is_recursive) {
-                    // recursive "leftover" remainder of a Nielsen substitution:
+                    // recursive "leftover" remainder of a Nielsen substitution
-                    // the substitution path captured all required characters, so
+                    // such as x -> [nth_u(x,k)] ++ x. If the variable still
-                    // the remaining occurrence is the empty string. Do NOT pad it
+                    // carries a primitive membership at the satisfying node
-                    // via get_var_value (the shared length belongs to the outer
+                    // (recorded in m_var_regex), the leftover is a genuine
-                    // variable, not this remainder).
+                    // non-empty witness of that residual regex, not an
-                    val = m_seq.str.mk_empty(curr->get_sort());
+                    // eliminated remainder. Otherwise the path drove it to the
+                    // empty string.
+                    if (m_var_regex.contains(curr->first()->id()))
+                        val = get_var_value(curr);
+                    else
+                        val = m_seq.str.mk_empty(curr->get_sort());
                 }
                 else {
                     // genuinely free variable (no replacement): respect its

src/smt/theory_nseq.cpp

@@ -296,7 +296,7 @@ namespace smt {
     void theory_nseq::assign_eh(bool_var v, bool is_true) {
         try {
             expr* e = ctx.bool_var2expr(v);
-            // std::cout << "assigned [" << sat::literal(v, is_true) << "] " << mk_pp(e, m) << " = " << is_true << std::endl;
+            std::cout << "assigned [" << sat::literal(v, is_true) << "] " << mk_pp(e, m) << " = " << is_true << std::endl;
             expr *s = nullptr, *re = nullptr, *a = nullptr, *b = nullptr;
             TRACE(seq, tout << (is_true ? "" : "¬") << mk_bounded_pp(e, m, 3) << "\n";);
             if (m_seq.str.is_in_re(e, s, re)) {
@@ -890,7 +890,7 @@ namespace smt {
         set_conflict(eqs, lits);
 
 #ifdef Z3DEBUG
-#if 0
+#if 1
         // Pass constraints to a subsolver to check correctness modulo legacy solver
         {
             smt_params p;