From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 8 May 2009 14:45:22 +0000 (+0000)
Subject: bug-fix. Disable rewritting multiplication by constants
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=0b14e1b6622078b840bd762ee7f2e12a8752cf68;p=francis%2Fstp.git

bug-fix. Disable rewritting multiplication by constants

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

diff --git a/simplifier/simplifier.cpp b/simplifier/simplifier.cpp
index d0a5cdf..2aa88b5 100644
--- a/simplifier/simplifier.cpp
+++ b/simplifier/simplifier.cpp
@@ -1084,7 +1084,14 @@ namespace BEEV {
       const ASTNode& n0 = inputterm.GetChildren()[0];
       const ASTNode& n1 = inputterm.GetChildren()[1];
 
-      if (BVCONST == n0.GetKind() ^ BVCONST == n1.GetKind())
+      // This implementation has two problems.
+      // 1) It causes a segfault for cmu-model15,16,17
+      // 2) It doesn't count the number of bits saved, so if there is a single
+      // leading bit it will invert it. Even though that will take more shifts
+      // and adds when it's finally done.
+
+      // disabled.
+      if (false && (BVCONST == n0.GetKind()) ^ (BVCONST == n1.GetKind()))
       {
       		CBV constant = (BVCONST == n0.GetKind())? n0.GetBVConst(): n1.GetBVConst();
       		ASTNode other = (BVCONST == n0.GetKind())? n1: n0;