Introducing term enumeration.

This commit introduces `leon.purescala.DataGen`, an object that contains
two static methods; `generate` and `findModels`. `generate` is a term
generator based on composition of streams. It can generate hundreds of
instances of recursive types in less than a tenth of a second.
`findModels` leverages `generate` to perform (small-)model finding. Pass
it an expression and an evaluator (preferably `CodeGenEvaluator`) and
watch it find models to your formula.

The commit also includes a small regression test suite.

(Note that although we have currently no use for this, the `generate`
function can in principle be used to generate arbitrary terms. E.g. you
could pass variables as fixed generators for certain types.)
Support for LetTuple in Fairz3
Completes Justify testcase

This commit completes the Justify testcase with some more
advanced properties.

It provides both an implementation with its specification for
verification, and a synthesis benchmark where choose is used
to try to derive the correct implementation.
Add various synthesis benchmarks
Implement --manual search mode
Improved, cached, datagen
Safer transitiveCall*, implement isInductive check
Compile functions with their pre/post conditions
ADTDual and Unification become normalizing rules
Implement ADTLongInduction and DetupleInput rules
Implement untrusted solutions, that are then validated
Fix PC being ignored by Synthesizer
Fix pc being propagated to ADTSplit's sub problems
Check whether pc to ADTInduction is inductive before propagating it
Filter non-det program whenever the tests exclude most paths

In case of timeout when searching for a counter-example, CEGIS will
consider the tentative solution as valid but untrusted. This untrusted
solution will then be validated within the complete solution.
Add synthesis suite, which tests synthesis application trees
Remove debug output, fix&improve testing suite
Introduces purely functional array benchmarks

This commit use array with a purely functional styles to process them.
In particular, it uses recursive function instead of while loop.
Those benchmarks are easier to debug than the equivalent ones relying
on imperative features, because they do not go through any code
transformations.

Note that they still have the same limitation as the imperative ones
(cannot prove inductive properties), which shows that the imperative
transformation are not responsible for the limitation in proving
validity of program over arrays.
Fix crash from IntegerInequalities due to non-linear formulas
Decouple the validation, group VCs per functions

Decoupling the validation phase allows the web-interface to interract in
a much easier way.

Grouping VCs per functions makes the verification overview easier.