fix #3525

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/ast.cpp

@@ -1794,6 +1794,15 @@ bool ast_manager::slow_not_contains(ast const * n) {
 }
 #endif
 
+#if 0
+static unsigned s_count = 0;
+static void track_id(ast* n, unsigned id) {
+    if (n->get_id() != id) return;
+    ++s_count;
+    std::cout << s_count << "\n";
+//    SASSERT(s_count != 7);
+}
+#endif
 
 ast * ast_manager::register_node_core(ast * n) {
     unsigned h = get_node_hash(n);

src/smt/theory_seq.cpp

@@ -3485,6 +3485,10 @@ bool theory_seq::solve_nc(unsigned idx) {
     lbool is_gt = ctx.get_assignment(len_gt);
     TRACE("seq", ctx.display_literal_smt2(tout << len_gt << " := " << is_gt << "\n", len_gt) << "\n";);
 
+    if (canonizes(false, n.contains())) {
+        return true;
+    }
+    
     switch (is_gt) {
     case l_true:
         add_length_to_eqc(a);
@@ -3494,18 +3498,41 @@ bool theory_seq::solve_nc(unsigned idx) {
         ctx.mark_as_relevant(len_gt);
         m_new_propagation = true;
         return false;
-    case l_false: {
+    case l_false: 
-        mk_decompose(a, head, tail);
+        break;
-        pre = mk_literal(m_util.str.mk_prefix(b, a));
+    }
-        cnt = mk_literal(n.contains());
+#if 0
-        ctail = mk_literal(m_util.str.mk_contains(tail, b));
+    expr_ref a1(m), b1(m);
-        emp = mk_literal(m_util.str.mk_is_empty(a));
+    dependency* deps = n.deps();    
-        add_axiom(cnt, ~pre);
+    if (!canonize(a, deps, a1)) {
-        add_axiom(cnt, ~ctail);
+        return false;
-        add_axiom(emp, mk_eq(a, m_util.str.mk_concat(head, tail), false));
+    }
+    if (!canonize(b, deps, b1)) {
+        return false;
+    }
+    if (a != a1 || b != b1) {
+        literal_vector lits;
+        expr_ref c(m_util.str.mk_contains(a1, b1), m);
+        propagate_eq(deps, lits, c, n.contains(), false);
+        m_ncs.push_back(nc(c, len_gt, deps));       
+        m_new_propagation = true;
         return true;
     }
-    }
+    IF_VERBOSE(0, verbose_stream() << n.contains() << "\n");
+#endif    
+    mk_decompose(a, head, tail);
+    expr_ref pref(m_util.str.mk_prefix(b, a), m);
+    expr_ref postf(m_util.str.mk_contains(tail, b), m);
+    m_rewrite(pref);
+    m_rewrite(postf);
+    pre = mk_literal(pref);
+    cnt = mk_literal(n.contains());
+    ctail = mk_literal(postf);
+    emp = mk_literal(m_util.str.mk_is_empty(a));
+    add_axiom(cnt, ~pre);
+    add_axiom(cnt, ~ctail);
+    add_axiom(emp, mk_eq(a, m_util.str.mk_concat(head, tail), false));
+    return true;
     
 #else
     dependency* deps = n.deps();    
@@ -3517,7 +3544,10 @@ bool theory_seq::solve_nc(unsigned idx) {
     CTRACE("seq", c != n.contains(), 
            tout << n.contains() << " =>\n" << c << "\n";
            display_deps(tout, deps););    
-
+    if (c != n.contains()) {
+        IF_VERBOSE(0, verbose_stream() << n.contains() << " =>\n" << c << "\n";
+                   display_deps(verbose_stream(), deps););
+    }
     
     if (m.is_true(c)) {
         literal_vector lits;

src/tactic/core/dom_simplify_tactic.cpp

@@ -392,8 +392,8 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
             }
             CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";);
             change |= r != g.form(i);
-            proof* new_pr = nullptr;
+            proof_ref new_pr(m);
-            if (g.proofs_enabled()) {
+            if (g.proofs_enabled() && g.pr(i)) {
                 new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(g.form(i), r));
             }
             g.update(i, r, new_pr, g.dep(i));
@@ -412,9 +412,10 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
             }
             change |= r != g.form(i);
             CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";);
-            proof* new_pr = nullptr;
+            proof_ref new_pr(m);
-            if (g.proofs_enabled()) {
+            if (g.proofs_enabled() && g.pr(i)) {
-                new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(g.form(i), r));
+                new_pr = m.mk_rewrite(g.form(i), r);
+                new_pr = m.mk_modus_ponens(g.pr(i), new_pr);
             }
             g.update(i, r, new_pr, g.dep(i));
         }