From 43cf0530664ba62e77e590b56133b07d463a1f6b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Jul 2022 15:43:12 -0700 Subject: [PATCH] fix #6128 --- src/smt/smt_model_checker.cpp | 2 +- src/smt/theory_array_full.cpp | 9 ++++++--- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 5f6131f59f2..90ef225a5ee 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -258,7 +258,7 @@ namespace smt { bindings.set(num_decls - i - 1, sk_value); } - TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: " << bindings << "\n" << defs << "\n";); + TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: " << bindings << "\ndefs:\n" << defs << "\n";); if (!defs.empty()) def = mk_and(defs); max_generation = std::max(m_qm->get_generation(q), max_generation); add_instance(q, bindings, max_generation, def.get()); diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 1a793a116f9..4311ef32c1c 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -594,10 +594,13 @@ namespace smt { if (!ctx.add_fingerprint(this, m_default_lambda_fingerprint, 1, &arr)) return false; m_stats.m_num_default_lambda_axiom++; - expr* def = mk_default(arr->get_expr()); + expr* e = arr->get_expr(); + expr* def = mk_default(e); quantifier* lam = m.is_lambda_def(arr->get_decl()); - expr_ref_vector args(m); - args.push_back(lam); + TRACE("array", tout << mk_pp(lam, m) << "\n" << mk_pp(e, m) << "\n"); + expr_ref_vector args(m); + var_subst subst(m, false); + args.push_back(subst(lam, to_app(e)->get_num_args(), to_app(e)->get_args())); for (unsigned i = 0; i < lam->get_num_decls(); ++i) args.push_back(mk_epsilon(lam->get_decl_sort(i)).first); expr_ref val(mk_select(args), m);