This new phase is invoked after the extraction phase. It will rewrite
precondition (and postcondition) of functions to add instanceOf when the
parameter (and return type) is a case class concrete type (instead of abstract
class).

If not done, then during the mapping to Z3 we lose the precise subtype
information, and Z3 will be able to find non valid counter-examples,
of a different case class for example.

Since tests are very important, we introduce two testcases that make
sure the issue is fixed. We also needed to update the Testcase runners
to make use of the new pipeline.

Removes old README file which has been subsumed
by the new README.md. Everything should be in .md anyway.

Choose was introduced after imperative transformation
and was not adapted to the transformation rule.

Since Choose can introduce a scope, val defined
inside its body should not be hoisted outside.

The functional ones are taken from previous collections (SAS2011 and
OOPSLA13 submission for Sorting).

The imperative ones are based on testcases from the VSTTE competition
and adaptations of functional benchmarks of SAS.  We are not able to
reproduce all successfull properties of the functional benchmarks,
especially when the function we are implementating was not originally
tail recursive. In that case, a non-trivial encoding would be required
(e.g. using accumulators).

Insertion sort and other sort algorithms are particularly complicated to
implement with an imperative style. Functions like `insert` need to use
reversal while reconstructing the list, and need in particular to prove
that reversing an increasing list yields a decreasing list. We are not
able to prove that yet.

(Challenging benchmarks currently beyond our reach are in the top-level
testcases directory, as they are not part of the Scala 2013 submission.)

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

Grouping VCs per functions makes the verification overview easier.

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.

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.

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.

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.)

- Choose expressions becomes uninterpreted functions under the same
  constraints.

- Fix bug with variablesOf considering choose binders as free.

- Silence evaluator errors when occuring with tentative lucky models.
  Note that choose expressions cannot be evaluated nor compiled.

Z3 may return an id->id model for array kinds, leading to an assertion
error caused by the expectation of getting an array literal. We
shortcircuit with z3IdToExpr to catch such cases for all kinds.