mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

disable conflicts logging by default

Browse source
This commit is contained in:
Jakob Rath 2023-03-17 23:37:32 +01:00
parent a10a7e31a6
commit 931e6d655e
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/conflict.cpp
View file

@ -54,6 +54,8 @@ TODO:
#include "math/polysat/variable_elimination.h" #include "math/polysat/variable_elimination.h"
#include <algorithm> #include <algorithm>
#define ENABLE_CONFLICTS_TXT 0
namespace polysat { namespace polysat {
class conflict_resolver { class conflict_resolver {
@ -130,7 +132,7 @@ namespace polysat {
conflict::conflict(solver& s) : s(s) { conflict::conflict(solver& s) : s(s) {
// TODO: m_log_conflicts is always false even if "polysat.log_conflicts=true" is given on the command line // TODO: m_log_conflicts is always false even if "polysat.log_conflicts=true" is given on the command line
if (true || s.get_config().m_log_conflicts) if (ENABLE_CONFLICTS_TXT || s.get_config().m_log_conflicts)
m_logger = alloc(file_inference_logger, s); m_logger = alloc(file_inference_logger, s);
else else
m_logger = alloc(dummy_inference_logger); m_logger = alloc(dummy_inference_logger);