mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

fix #3302

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-14 14:39:03 -07:00
parent ec0349819f
commit 42dbee9165
1 changed files with 14 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/smt/smt_model_checker.cpp
View file

@ -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";