EnumerationSolver/Portfolio extends Incremental+Assumption

This allows us to use them in synthesis. Expose --solvers=..
option for synthesis.
Allow testing specifying options, add test for enum solver
Improve types, support ???[T] as all-seeing choose

- Holes become chooses

- Unhandled types are removed, Untyped is now checked for and
  a warning is issued if an untyped expression is found.
Add rule for splitting ifs in predicates
Disambiguate for direct use within Play
Fix positions of holes and resulting chooses
Indirection for inlining to prevent duplicate clauses being issued to Z3
Move condition abduction to a feature branch
Make vanuatoo more resilient to non-patternable Exprs
Make sure the current directory is not within the class path
Refactor reporters, allow positions which will get printed with lines
All-seeing synthesis with Oracles, library reorganisation

- NormalizationRule becomes priorities, so that we can have multiple
  distinct layers

- Use the @library annotation, move synthesis stuff to synthesis,
  Oracles.

- Make sure tests use PreprocessingPhase and import synthesis when
  adequate

- Extract proper package objects fix patternRecons and simplifiers

- Reorganize library:
  - leon.{choose,???} -> leon.lang.synthesis
  - leon.{waypoint,epsilon} -> leon.lang.xlang
Corrected some issues with termination proving.
Improve test reporting in case of fatal errors
Refactor tests to make them more stable
Actually add the files
Making sure all errors are kept
Fix bugs related to LetTuples not being handled
Add BinarySearchTree with isSorted and buggyMerge
New Ensuring/Require/Assert trees

- Ensurings/Require are now proper purescala trees
- Introduce Assert as a tree
- Simplify tactics to support arbitrary asserts/errors/inner ensurings
- New phase to inject assertions for unsafe calls (array/map access)
- Refactor Default and Induction tactic