probably won't fix #6127

recfun decl plugin does not get copied so recursive functions are lost when cloning.
Fix is risky and use case is limited to threads + recursive definitions

src/smt/theory_recfun.cpp

@@ -43,32 +43,32 @@ namespace smt {
 
     char const * theory_recfun::get_name() const { return "recfun"; }
 
-    theory* theory_recfun::mk_fresh(context* new_ctx) {
+    theory* theory_recfun::mk_fresh(context* new_ctx) {        
         return alloc(theory_recfun, *new_ctx);
     }
 
     bool theory_recfun::internalize_atom(app * atom, bool gate_ctx) {
+        TRACE("recfun", tout << mk_pp(atom, m) << " " << u().has_defs() << "\n");
         if (!u().has_defs()) {
+//            if (u().is_defined(atom)) 
+//                throw default_exception("recursive atom definition is out of scope");
             return false;
         }
-        for (expr * arg : *atom) {
+        for (expr * arg : *atom) 
             ctx.internalize(arg, false);
-        }
-        if (!ctx.e_internalized(atom)) {
+        if (!ctx.e_internalized(atom)) 
             ctx.mk_enode(atom, false, true, true);
-        }
-        if (!ctx.b_internalized(atom)) {
-            bool_var v = ctx.mk_bool_var(atom);
-            ctx.set_var_theory(v, get_id());
-        }
-        if (!ctx.relevancy() && u().is_defined(atom)) {
+        if (!ctx.b_internalized(atom)) 
+            ctx.set_var_theory(ctx.mk_bool_var(atom), get_id());
+        if (!ctx.relevancy() && u().is_defined(atom)) 
             push_case_expand(atom);
-        }
         return true;
     }
 
     bool theory_recfun::internalize_term(app * term) {
         if (!u().has_defs()) {
+//            if (u().is_defined(term)) 
+//                throw default_exception("recursive term definition is out of scope");
             return false;
         }
         for (expr* e : *term) {