mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

virtual_solver: debug print

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-21 15:47:28 -07:00
parent 891dcd99c2
commit 56bce005a0
1 changed files with 8 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/muz/spacer/spacer_virtual_solver.cpp
View file

@ -150,7 +150,6 @@ lbool virtual_solver::check_sat_core(unsigned num_assumptions,
st.update("time", sw.get_seconds());
st.display_smt2(out);
out.close();
if (m_factory.fparams().m_dump_recheck) {
scoped_no_proof _no_proof_(m);
@ -164,7 +163,13 @@ lbool virtual_solver::check_sat_core(unsigned num_assumptions,
sw2.stop();
verbose_stream() << file_name.str() << " :orig "
<< sw.get_seconds() << " :new " << sw2.get_seconds();
out << ";; :orig " << sw.get_seconds()
<< " :new " << sw2.get_seconds() << "\n"
<< ";; :new is time to solve with fresh smt::kernel\n";
}
out.close();
}
@ -195,9 +200,9 @@ void virtual_solver::pop_core(unsigned n) {
SASSERT(!m_in_delay_scope);
m_context.pop(n);
m_pushed = get_scope_level() - n > 0;
}
}
else {
m_in_delay_scope = get_scope_level() - n > 0;
m_in_delay_scope = get_scope_level() - n > 0;
}
}