From 23685aaa56ed97b76b2740172ee29b80956723f8 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 9 Feb 2012 00:35:43 +0000
Subject: [PATCH] Disable bit-blast equivalence checking, it returns the wrong
 answer sometimes.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1565 e59a4935-1847-0410-ae03-e826735625c1
---
 src/STPManager/STP.cpp | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 8f9bb6f..e6c0e02 100644
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -114,6 +114,7 @@ namespace BEEV {
         ASTNodeMap fromTo;
         ASTNodeMap equivs;
         bb.getConsts(simplified_solved_InputToSAT, fromTo,equivs);
+#if 0
         if (equivs.size() > 0)
           {
             /* These nodes have equivalent AIG representations, so even though they have different
@@ -124,7 +125,7 @@ namespace BEEV {
              * difficult looking ASTNodes.
             */
             //cerr << "eQUIV";
-#if 0
+
             ASTNodeMap::iterator it = equivs.begin();
             while (it!=equivs.end())
               {
@@ -133,12 +134,12 @@ namespace BEEV {
                 cerr << it->second << endl;
                 it++;
               }
-#endif
+
             ASTNodeMap cache;
             simplified_solved_InputToSAT = SubstitutionMap::simple_replace(simplified_solved_InputToSAT, equivs, cache,&nf);
             bm->ASTNodeStats(bb_message.c_str(), simplified_solved_InputToSAT);
           }
-
+#endif
         if (fromTo.size() > 0)
           {
             ASTNodeMap cache;
-- 
2.47.3