From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 19 Apr 2009 13:05:21 +0000 (+0000)
Subject: small bug fixes for problems introduced the last checkin.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=ef0cd9e87a651f88b5657a4accac1d191023a8df;p=francis%2Fstp.git

small bug fixes for problems introduced the last checkin.



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

diff --git a/simplifier/simplifier.cpp b/simplifier/simplifier.cpp
index ff0e4dc..81729e2 100644
--- a/simplifier/simplifier.cpp
+++ b/simplifier/simplifier.cpp
@@ -1125,11 +1125,8 @@ namespace BEEV {
       const ASTNode& n0 = inputterm.GetChildren()[0];
       const ASTNode& n1 = inputterm.GetChildren()[1];
       
-      if (BVCONST == n0.GetKind() || BVCONST == n1.GetKind())
+      if (BVCONST == n0.GetKind() ^ BVCONST == n1.GetKind())
       {
-      		// assuming that if both are constants it is handled already.
-      		assert(BVCONST == n0.GetKind() ^ BVCONST == n1.GetKind());
-      	
       		CBV constant = (BVCONST == n0.GetKind())? n0.GetBVConst(): n1.GetBVConst();
       		ASTNode other = (BVCONST == n0.GetKind())? n1: n0;
       		
@@ -1150,7 +1147,7 @@ namespace BEEV {
       					CONSTANTBV::BitVector_Bit_On(maskedPlusOne, i);
       			}
       			CONSTANTBV::BitVector_increment(maskedPlusOne);
-      			ASTNode& temp = CreateTerm(BVMULT,inputValueWidth, CreateBVConst(maskedPlusOne,inputValueWidth),other);
+      			ASTNode temp = CreateTerm(BVMULT,inputValueWidth, CreateBVConst(maskedPlusOne,inputValueWidth),other);
       			output = CreateTerm(BVNEG, inputValueWidth, temp); 
       		}
       }