[SMT-LIB] QF_UFBV[32]

[Clark Barrett]

I have posted a large set of QF_UFBV[32] benchmarks on the SMT-LIB benchmark
web page.  In order to translate these benchmarks, I had to add a couple of
extensions to the logic.

The following operators have been added: sbvlt, sbvleq, sbvgt, sbvgeq, sign_extend.
The first four are the signed comparison operators.  The sign_extend operator
simply extends the bitvector with copies of its most-significant bit.  You will
need to add these operators to your parsers to parse all of the benchmarks.

Formal definitions of all the new operators can be found in the QF_UFBV[32]
logic definition.

I also made one fix to the theory: the definition of bvneg was changed to be
consistent with bvsub.  Note that bit-wise negation is represented using bvnot,
not bvneg.

Let me know if you have any questions about the changes or the new benchmarks.

-Clark Barrett