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

remove debug code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-22 13:57:09 +01:00
parent bceff4b3fa
commit 73060ecaec
1 changed files with 0 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/sat/sat_solver.cpp
View file

@ -36,8 +36,6 @@ Revision History:
namespace sat {
static unsigned s_lemma_count = 0;
static bool s_verify_contains = false;
solver::solver(params_ref const & p, reslimit& l):
solver_core(l),
@ -388,9 +386,6 @@ namespace sat {
if (!learned && !at_search_lvl())
m_clauses_to_reinit.push_back(clause_wrapper(l1, l2));
}
if (l1 == literal(29327, false) && l2 == literal(29328, false)) {
std::cout << s_lemma_count << "\n";
}
m_stats.m_mk_bin_clause++;
get_wlist(~l1).push_back(watched(l2, learned));
get_wlist(~l2).push_back(watched(l1, learned));
@ -2422,20 +2417,6 @@ namespace sat {
}
}
s_lemma_count++;
if (s_lemma_count == 51802) {
disable_trace("sat");
disable_trace("sat_conflict");
s_verify_contains = false;
}
if (s_lemma_count == 51801) {
enable_trace("sat");
enable_trace("sat_conflict");
s_verify_contains = true;
}
m_lemma.reset();
@ -2458,8 +2439,6 @@ namespace sat {
TRACE("sat_conflict_detail", tout << "processing consequent: " << consequent << "\n";
tout << "num_marks: " << num_marks << ", js: " << js << "\n";);
// VERIFY(!s_verify_contains || !m_config.m_drat || m_drat.contains(consequent, js));
switch (js.get_kind()) {
case justification::NONE:
break;