From e5c6620767423d81db449bed452015dfbdd89389 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 9 Jul 2010 14:06:23 +0000
Subject: [PATCH] Decision. This optimisation helps our cvc regressions but
 hurts our smtlib ones. So I'm taking it out..

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@943 e59a4935-1847-0410-ae03-e826735625c1
---
 src/simplifier/simplifier.cpp | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 93cee1e..4e42875 100644
--- 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])
-- 
2.47.3