From 32e0493affc0279ab38e193bf29c3fbd12c2ad31 Mon Sep 17 00:00:00 2001
From: msoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 5 Jul 2010 08:48:57 +0000
Subject: [PATCH] For low-cutoff speed reasons, it's best not to subsume
 learnts

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@924 e59a4935-1847-0410-ae03-e826735625c1
---
 src/sat/cryptominisat2/Subsumer.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/sat/cryptominisat2/Subsumer.cpp b/src/sat/cryptominisat2/Subsumer.cpp
index 27126c2..1b056c0 100644
--- a/src/sat/cryptominisat2/Subsumer.cpp
+++ b/src/sat/cryptominisat2/Subsumer.cpp
@@ -1148,8 +1148,8 @@ const bool Subsumer::simplifyBySubsumption(const bool alsoLearnt)
     else fullSubsume = false;
     if (alsoLearnt) fullSubsume = true;
 
-    solver.clauseCleaner->cleanClauses(solver.learnts, ClauseCleaner::learnts);
-    addFromSolver<true>(solver.learnts, alsoLearnt);
+    //solver.clauseCleaner->cleanClauses(solver.learnts, ClauseCleaner::learnts);
+    //addFromSolver<true>(solver.learnts, alsoLearnt);
     solver.clauseCleaner->cleanClauses(solver.clauses, ClauseCleaner::clauses);
     addFromSolver<true>(solver.clauses, alsoLearnt);
 
-- 
2.47.3