Decision. This optimisation helps our cvc regressions but hurts our smtlib ones....

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@943 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 93cee1edcda59a0bfbe80b26913eb8e98c2a2adb..4e42875941a34615fe3f4eb2f67e4cfbb1abef5d 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -2120,12 +2120,19 @@ namespace BEEV
                   }
                 break;
               }
+
+          // This can increase the number of nodes exponentially.
+          // If turned on bitrev2048 will blow out main memory, with
+          // this disabled it takes 12MB.
+              #if 0
+
             case BVAND:
             case BVOR:
             case BVXOR:
               {
                assert(a0.Degree() == 2);
-                //assumes these operators are binary
+
+               //assumes these operators are binary
                 //
                 // (t op u)[i:j] <==> t[i:j] op u[i:j]
                 ASTNode t = a0[0];
@@ -2140,9 +2147,12 @@ namespace BEEV
                                VarConstMap);
                 BVTypeCheck(t);
                 BVTypeCheck(u);
-                output = nf->CreateTerm(k1, a_len, t, u);
+                //output = nf->CreateTerm(k1, a_len, t, u);
+
+                output = inputterm;
                 break;
               }
+          #endif
             case BVNEG:
               {
                 // (~t)[i:j] <==> ~(t[i:j])