From: msoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 26 Jul 2010 12:21:20 +0000 (+0000)
Subject: Further fixing of spurious printing in CryptoMiniSat
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=8af604504aa752f0691307f1a1c02958fa1861c5;p=francis%2Fstp.git

Further fixing of spurious printing in CryptoMiniSat

As per report by Trevor Hansen

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@953 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/src/sat/cryptominisat2/XorSubsumer.cpp b/src/sat/cryptominisat2/XorSubsumer.cpp
index d1f6dd8..dc5c4fb 100644
--- a/src/sat/cryptominisat2/XorSubsumer.cpp
+++ b/src/sat/cryptominisat2/XorSubsumer.cpp
@@ -474,7 +474,6 @@ const bool XorSubsumer::simplifyBySubsumption(const bool doFullSubsume)
         propagated =  (solver.qhead != solver.trail.size());
         solver.ok = (solver.propagate().isNULL());
         if (!solver.ok) {
-            std::cout << "c (contradiction during subsumption)" << std::endl;
             return false;
         }
         solver.clauseCleaner->cleanXorClausesBewareNULL(clauses, ClauseCleaner::xorSimpClauses, *this);