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 ff0e4dc1e37151d9e0af98753db53e4109874ebb..81729e21ae56ed2ce47b72066e01119b166bfd26 100644 (file)
--- 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); 
                }
       }