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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 8f9bb6fcee18839c29c639ce20ae3ecea667c7f9..e6c0e02f5584f2cd88c6083ca6f221712622197d 100644 (file)
--- 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;