From ed0b57ea9618ff2bfe6df21d7e2cc983132fe5a2 Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 10 Dec 2009 16:38:33 +0000
Subject: [PATCH] made -fPIC and -march=native optional

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@498 e59a4935-1847-0410-ae03-e826735625c1
---
 scripts/Makefile.common |  3 ++-
 src/to-sat/BitBlast.cpp |  3 ++-
 src/to-sat/SimpBool.cpp | 11 -----------
 src/to-sat/ToSAT.cpp    |  2 +-
 4 files changed, 5 insertions(+), 14 deletions(-)

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 70d7bc5..4f8674a 100644
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -10,7 +10,8 @@
 
 #OPTIMIZE     = -g -pg            # Debugging and gprof-style profiling
 OPTIMIZE      = -g                # Debugging
-OPTIMIZE      = -O3 -fPIC         # Maximum optimization
+OPTIMIZE      = -O3               # Maximum optimization
+#OPTIMIZE      = -O3 -fPIC         # Maximum optimization
 #OPTIMIZE      = -O3 -march=native # Maximum optimization
 #OPTIMIZE     = -O3 -march=native -DNDEBUG -DLESSBYTES_PERNODE
 #CFLAGS_M32   = -m32
diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index 8eac631..fa116bd 100644
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -1034,7 +1034,8 @@ namespace BEEV
         }
       case BVGT:
         {
-          return _bm->CreateSimpNot(BBBVLE(left, right, false));
+          //return _bm->CreateSimpNot(BBBVLE(left, right, false));
+          return BBBVLE(right, left, false, true);
           break;
         }
       case BVLT:
diff --git a/src/to-sat/SimpBool.cpp b/src/to-sat/SimpBool.cpp
index 273b46a..fa45931 100644
--- a/src/to-sat/SimpBool.cpp
+++ b/src/to-sat/SimpBool.cpp
@@ -481,17 +481,6 @@ namespace BEEV
       {
         retval = CreateSimpAndOr(1, child0, child1);
       }
-//     //ITE (x, !y, y) == x XOR y
-//     else if (NOT == child1.GetKind() && (child1[0] == child2))
-//       {
-// 	retval = CreateSimpXor(child0, child2);
-//       }
-//     // ITE (x, y, !y) == x IFF y.  I think other cases are covered
-//     // by XOR/IFF optimizations
-//     else if (NOT == child2.GetKind() && (child2[0] == child1)) 
-//       {
-// 	retval = CreateSimpXor(CreateSimpNot(child0), child2);
-//       }
     else
       {
 	ASTNode left  = CreateNode(AND, child0, child1);
diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 3a257cb..d2ac1e9 100644
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -137,7 +137,7 @@ namespace BEEV
 
 #if defined CRYPTOMINISAT2
 	newSolver.set_gaussian_decision_until(100);
-	newSolver.performReplace = false;
+	newSolver.performReplace = true;
 	newSolver.xorFinder = false;
 #endif
 
-- 
2.47.3