Improving naming of bit-vector signed division constants.

This renaming introduces incompatibilities:

• words$word_sdiv -> words$word_quot (this is proved to be related to int_quot for a non-zero divisor).
• words$word_srem -> words$word_rem (this is proved to be related to int_rem for a non-zero divisor).
• integer_word$word_sdiv (this is a new constant defined directly in terms of int_div).
• words$word_smod -> integer_word$word_smod (this is now defined directly in terms of int_mod).

Tuned.

word_smod and bvsmod are mapped to each other again.

word_smod and bvsmod are no longer mapped to each other: they are semantically
different functions.

Added (partial) support for shift operations that take two word arguments.

Major update, adding a translation from HOL to SMT-LIB 2 and enabling Z3 proof
checking again. (The latter still has some quirks, because Z3's proof
syntax is not fully SMT-LIB 2 compliant.)

Added SMT-LIB parsing support for QF_UFNRA, UFLRA, UFNIA.

Added SMT-LIB parsing support for QF_UFLRA.

Added SMT-LIB parsing support for QF_UFLIA.

Added SMT-LIB parsing support for QF_NRA.

Added SMT-LIB parsing support for QF_UFBV.

Z3 proof parser updated for Z3 2.13. The proof parser now uses the SMT-LIB
benchmark parser internally.

Added parsing support for bvcomp.

Added parsing support for bvsrem and bvsmod.

Added parsing support for bvsdiv.

Added a parser for SMT-LIB 2 benchmarks.