Left shift, >32 bit constants, fixed zero_extend, fixed (?) SBVREM.

Left shift, >32 bit constants, fixed zero_extend, fixed (?) SBVREM.

Now left shifts by a variable amount. Previously the shift amount needed to a constant.

The smtlib parser reads bitvector constants into strings rather than into ints. This allows formula to
contain constants greater than the size of the machine's integer.

Fixed zero_extend. I didn't add code for it into the SimplifyTermAux function. SBVREM was sometimes failing
because it also wasn't included in the same function. Added it in. Not sure what the function does though..

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