From 6ed2b444b5a679b1cb6dd0502dab227f1cf1468f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Jul 2022 18:10:52 -0700 Subject: [PATCH] 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 | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index c18e5577b92..4162752759e 100644 --- a/src/smt/theory_recfun.cpp +++ b/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) {