[SMT-LIB] new bitvector theories/logics

[Clark Barrett]

If you look at the files I posted, you'll see that these operators have already
been renamed as you suggested.  I would appreciate it if you would take a
careful look at the summary in QF_BV.smt and let me know if you have any
additional feedback.

-Clark

> 
> Hi Clark,
> 
> Thx for accepting my suggestion about naming comparison operators bv(u|s)xx,
> that's much more consistent.
> 
> Question: Are you also planning to rename div & rem operators:
> 
> bvdiv -> bvudiv
> bvsdiv stays the same
> bvrem -> bvurem
> bvsrem stays the same
> 
> These additional renamings would make the theory more consistent.
> 
> Domagoj Babic
>