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

remove cond-log use

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-20 16:11:05 -07:00
parent 8ee54c665a
commit 32c3a3e3cc
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/solver.cpp
View file

@ -63,7 +63,7 @@ namespace polysat {
LOG_H1("Next solving loop iteration (#" << m_stats.m_num_iterations << ")");
LOG("Free variables: " << m_free_pvars);
LOG("Assignment: " << assignments_pp(*this));
COND_LOG(is_conflict(), "Conflict: " << m_conflict);
if (is_conflict()) LOG("Conflict: " << m_conflict);
IF_LOGGING(m_viable.log());
if (!is_conflict() && m_constraints.should_gc()) m_constraints.gc(*this);
else if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; }