(b) Removing an unproven axiom on conqueue
(c) Adding a free variable factory. Need to incorporate it so as to assert
freshness of newly created closures

(b) Added 3 strategies for Conqueue, two of which is verifiable.
   The best strategy still has one unverified (but simple) axiom
   that relies on the acyclicity of streams
(c) Improved the model and fixed some bugs.

(b) Adding an option: unfoldFactor to unfold functions more than once in each iteration of verification

Solvers are no longer distinguished in 20 traits depending on what they
implement. It turns out that most leon solvers already implemented
everything:

1) Being interrupted
2) Push / Pop
3) checkAssertions/getUnsatCore (a naive implementation of these
   can be added by mixing NaiveAssumptionSolver in)

- solvers are not freed directly, they are reclaimed by their
  solver factory

- reset() is used when available to reset a solver instead of creating a
  fresh one.

Implies(pre, f(x) = body)

becomes, with (--assumepre):

And(pre, f(x) = body)

- Command line option definitions are now represented by a type
  parametric class.
- Components can declare legal option definitions.
- Options are parsed according to those definitions in Main,
  and stored in LeonContext.
- Components can then retrieve back the options from LeonContext.
  This is not perfect, as it requires some type casts.
- leon.Settings only contained redundant information and has been
  removed.
- Unused options from SynthesisSettings have been removed.