From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 9 Feb 2012 00:35:43 +0000 (+0000)
Subject: Disable bit-blast equivalence checking, it returns the wrong answer sometimes.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=23685aaa56ed97b76b2740172ee29b80956723f8;p=francis%2Fstp.git

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 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;