mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-03 01:40:22 +00:00
Code Activity

fix #6128

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-07-12 15:43:12 -07:00
parent faf6c02cf8
commit 43cf053066
2 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_model_checker.cpp
View file

@ -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());