Allow >32-bit bit-vector constants on 32-bit machines.

The previous changes worked on 64-bit, not 32-bit machines. When I
compiled with -m32 it broke. This patch fixes it.

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

diff --git a/AST/AST.h b/AST/AST.h
index 27d090e0778793e57cfa6408d1cce987a85edbde..56dde97a32f84a3d9d013dc54fff13ac9cc2cef1 100644 (file)
--- a/AST/AST.h
+++ b/AST/AST.h
@@ -697,8 +697,8 @@ namespace BEEV {
        // It may only contain a small value in a bit type, which fits nicely into an unsigned int.
        // This is common for functions like: bvshl(bv1[128], bv1[128])
        // where both operands have the same type.
-       unsigned long maxBit = (unsigned) CONSTANTBV::Set_Max(n.GetBVConst());
-       if (maxBit >= sizeof(unsigned int) * 8 )
+       signed long maxBit = CONSTANTBV::Set_Max(n.GetBVConst());
+       if (maxBit >= ((signed long) sizeof(unsigned int)) * 8 )
          {
            n.LispPrint(cerr); //print the node so they can find it.
            FatalError("GetUnsignedConst: cannot convert bvconst of length greater than 32 to unsigned int");