From 42dbee9165d29737ef1adb1ca8c4850a508ef643 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Mar 2020 14:39:03 -0700 Subject: [PATCH] fix #3302 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_model_checker.cpp | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 235062955..d1030efdb 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -612,7 +612,20 @@ namespace smt { } if (inst.m_def) { - m_context->internalize_assertion(inst.m_def, nullptr, gen); + unsigned n = 1; + expr* const* args = &inst.m_def; + if (m.is_and(inst.m_def)) { + n = to_app(inst.m_def)->get_num_args(); + args = to_app(inst.m_def)->get_args(); + } + for (unsigned i = 0; i < n; ++i) { + proof* pr = nullptr; + expr* arg = args[i]; + if (m.proofs_enabled()) { + pr = m.mk_def_intro(arg); + } + m_context->internalize_assertion(arg, pr, gen); + } } TRACE("model_checker_bug_detail", tout << "instantiating... q:\n" << mk_pp(q, m) << "\n";