fix #4049

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

src/smt/smt_context.cpp

@@ -168,6 +168,10 @@ namespace smt {
 
         for (unsigned i = 0; !src_m.proofs_enabled() && i < src_ctx.m_assigned_literals.size(); ++i) {
             literal lit = src_ctx.m_assigned_literals[i];
+            bool_var_data const & d = src_ctx.get_bdata(lit.var());
+            if (d.is_theory_atom() && !src_ctx.m_theories.get_plugin(d.get_theory())->is_safe_to_copy(lit.var())) {
+                continue;
+            }
             expr_ref fml0(src_m), fml1(dst_m);
             src_ctx.literal2expr(lit, fml0);
             fml1 = tr(fml0.get());

src/smt/smt_parallel.cpp

@@ -183,7 +183,7 @@ namespace smt {
             }
         };
 
-        // num_threads = 1;
+        // for debugging: num_threads = 1;
 
         while (true) {
             vector<std::thread> threads(num_threads);

src/smt/smt_theory.h

@@ -404,6 +404,8 @@ namespace smt {
         bool is_representative(theory_var v) const {
             return get_representative(v) == v;
         }
+
+        virtual bool is_safe_to_copy(bool_var v) const { return true; }
 
         unsigned get_num_vars() const {
             return m_var2enode.size();

src/smt/theory_seq.cpp

@@ -1199,6 +1199,17 @@ bool theory_seq::reduce_length(unsigned i, unsigned j, bool front, expr_ref_vect
     }
 }
 
+/**
+   Skolem predicates for automata acceptance are stateful. 
+   They depend on the shape of automata that were used when the predicates
+   were created. It is unsafe to copy assertions about automata from one context
+   to another.
+*/
+bool theory_seq::is_safe_to_copy(bool_var v) const {
+    context & ctx = get_context();
+    expr* e = ctx.bool_var2expr(v);
+    return !m_sk.is_skolem(e);
+}
 
 bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
     context& ctx = get_context();
@@ -3352,6 +3363,7 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
     VERIFY(m_autil.is_numeral(idx, _idx));
     VERIFY(aut);
     if (aut->is_sink_state(src)) {
+        TRACE("seq", { display_expr d(m); aut->display(tout << "sink " << src << "\n", d); });
         propagate_lit(nullptr, 1, &lit, false_literal);
         return;
     }

src/smt/theory_seq.h

@@ -446,6 +446,7 @@ namespace smt {
         theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, new_ctx->get_manager(), m_params); }
         char const * get_name() const override { return "seq"; }
         bool include_func_interp(func_decl* f) override { return m_util.str.is_nth_u(f); }
+        bool is_safe_to_copy(bool_var v) const;
         theory_var mk_var(enode* n) override;
         void apply_sort_cnstr(enode* n, sort* s) override;
         void display(std::ostream & out) const override;