Adds a benchmark with many cool magic tricks with bits.
However, proving some of them is very costly and we
could potentially look at opportunities to make the proofs
go through faster.

Leon now matches Scala semantics of Int as 32 bits bit-vectors.
This commits modifies the semantics of IntLiteral to be treated
as 32 bits integer everywhere (solver, evaluator, ...).

Introduces a new literal type, InfiniteIntegerLiteral, representing
a natural integer. The front-end maps the use of BigInt to these
new trees, and the solver properly handles them as mathematical
integers.

The behaviour of many regression tests changes due to this new
semantics. In particular many of them now timeout because they
are no longer proving properties over mathematical integers. This
commit updates the tests to reflect this new semantics.

FiniteArray now takes an Expr for the length, a default
Expr, and a Map of defined Expr for some of its elements.
Adapt the rest of Leon to the new trees.

The PrettyPrinter tries to be a little bit smart about
how to print the array, only printing a few elements when the
array gets too big. The regression test produces an
huge array counter-example that used to lead to a crash of
Leon with the previous implementation of Array (fully represented
in memory).