- Activate through --cegis:vanuatoo
- Possibility to skip isomorphic models
- One pattern per conjunct

This commit introduces a proper hashCode function for case classes and
tuples used in codegen. It also changes the internal datastructure for
maps and sets from TreeX to HashX.

The new benchmark is a Heap, straight from Okasaki's PhD thesis.
Currently the specification is very weak ("implements a set").
The fix is the addition of a missing case (SubsetOf) in the evaluator.

- Refactor code extraction
  - Standardize extractors
  - Fix type identification by resolving type aliases

- Redo reporter integration with Scalac
  - Fix relining to prevent bizarre compile-errors

- Refactor Pretty-Printers
  - Extensible class interface
  - Not returning mutable string-buffers anymore

- Fixes according to 2.10
    - 100% false warnings in Tests
    - imports for postfix-ops or implicits

- Upgrade ScalaZ3 to 2.10

- Upgrade Cafebabe to 2.10

Fix typo

Fix some links/references

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.