From 160668cd2bab85640b8350e64c49d7fcd09c39c6 Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 5 Dec 2009 03:12:34 +0000
Subject: [PATCH] lots of changes aimed at CryptoMiniSAT2

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@455 e59a4935-1847-0410-ae03-e826735625c1
---
 src/sat/cryptominisat/Solver.cpp  | 1 +
 src/sat/cryptominisat2/Solver.cpp | 2 +-
 src/to-sat/BitBlast.cpp           | 3 +--
 src/to-sat/CallSAT.cpp            | 1 -
 src/to-sat/ToSAT.cpp              | 4 +++-
 5 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/sat/cryptominisat/Solver.cpp b/src/sat/cryptominisat/Solver.cpp
index 01a4d8a..b5c3af5 100644
--- a/src/sat/cryptominisat/Solver.cpp
+++ b/src/sat/cryptominisat/Solver.cpp
@@ -17,6 +17,7 @@ NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FO
 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
+
 #include "Solver.h"
 #include "Sort.h"
 #include <cmath>
diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp
index 46f7062..0cb5424 100644
--- a/src/sat/cryptominisat2/Solver.cpp
+++ b/src/sat/cryptominisat2/Solver.cpp
@@ -37,7 +37,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "Conglomerate.h"
 #include "XorFinder.h"
 
-#define DEBUG_LIB
+//#define DEBUG_LIB
 
 #ifdef DEBUG_LIB
 #include <sstream>
diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index a762e07..07d22dd 100644
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -6,7 +6,6 @@
  *
  * LICENSE: Please view LICENSE file in the home dir of this Program
  ********************************************************************/
-
 #include <cmath>
 #include <cassert>
 #include "../AST/AST.h"
@@ -968,7 +967,7 @@ namespace BEEV
         bit_comparisons.push_back(prev_eq_bit);
       }
     ASTNode output =
-      _bm->CreateSimpForm(OR, bit_comparisons);
+      _bm->CreateSimpForm(XOR, bit_comparisons);
 
     return output;
   }
diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp
index a3e7317..8a134a9 100644
--- a/src/to-sat/CallSAT.cpp
+++ b/src/to-sat/CallSAT.cpp
@@ -6,7 +6,6 @@
  *
  * LICENSE: Please view LICENSE file in the home dir of this Program
  ********************************************************************/
-
 #include "ToSAT.h"
 #define MAX_BUCKET_LIMIT 3
 
diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index de26935..c6d309a 100644
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -134,6 +134,8 @@ namespace BEEV
 
 #if defined CRYPTOMINISAT2
 	      newS.set_gaussian_decision_until(100);
+	      newS.performReplace = false;
+	      newS.xorFinder = false;
 #endif
               newS.solve();
             bm->GetRunTimes()->stop(RunTimes::Solving);
@@ -159,7 +161,7 @@ namespace BEEV
 
     bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
     bm->GetRunTimes()->start(RunTimes::Solving);
-
+    
     newS.solve();
     bm->GetRunTimes()->stop(RunTimes::Solving);
     bm->PrintStats(newS);
-- 
2.47.3