mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fixing bug causing unbalance between [instance] and [end-of-instance] lines

Browse source
This commit is contained in:
nilsbecker 2019-04-18 14:45:43 +02:00
parent 28ff338b88
commit 1c24d340d1
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/qi_queue.cpp
View file

@ -216,8 +216,10 @@ namespace smt {
if (m_manager.is_true(s_instance)) {
TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m_manager););
if (m_manager.has_trace_stream())
if (m_manager.has_trace_stream()) {
display_instance_profile(f, q, num_bindings, bindings, pr->get_id(), generation);
m_manager.trace_stream() << "[end-of-instance]\n";
}
return;
}