mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

increased verbosity level of smt_context

Browse source
This commit is contained in:
Arie Gurfinkel 2017-07-31 15:15:37 -04:00
parent ba6594b241
commit 9f9dc5e19f
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_context.cpp
View file

@ -3548,7 +3548,7 @@ namespace smt {
return false; return false;
} }
if (cmr == quantifier_manager::UNKNOWN) { if (cmr == quantifier_manager::UNKNOWN) {
IF_VERBOSE(1, verbose_stream() << "(smt.giveup quantifiers)\n";); IF_VERBOSE(2, verbose_stream() << "(smt.giveup quantifiers)\n";);
// giving up // giving up
m_last_search_failure = QUANTIFIERS; m_last_search_failure = QUANTIFIERS;
status = l_undef; status = l_undef;
@ -3558,7 +3558,7 @@ namespace smt {
inc_limits(); inc_limits();
if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) { if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) {
SASSERT(!inconsistent()); SASSERT(!inconsistent());
IF_VERBOSE(1, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations IF_VERBOSE(2, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations
<< " :decisions " << m_stats.m_num_decisions << " :decisions " << m_stats.m_num_decisions
<< " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold; << " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold;
if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) { if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) {