- Free&Recreate solvers during synthesis. This avoids huge memory leaks
  due to Z3AST never being reclaimed thourough the entire synthesis
  process

- Add safeguard to catch Z3Solvers for which memory management is
  incomplete

- Describe individual rule applications to allow a user to select one
  in particular

- Scala-Printing LetDefs correctly, allow initial indenting

- Fix Choose with single out variable not generating Tuple1

- Give synthesis a specific path to follow, used by web

- Allow val (x: Int, y: Int) = ... along with locally{}

- Expose information on the synthesis search tree

- Correctly substitute varaibles in ADTInduction's pre/post

- Generic transformers with PC tracking, collect chooses with PC

- Detect line indentation of choose() to indent solution correctly

- Implement simplifier which renames ids based on the context

- Rescale timeouts, use uninterpreted solver for filtering simple cases

- Assume that choose() can reference the entire scope

  This is necessary to ensure that Lets do not get thrown away. For
  instance:

  Let(x = ..., choose(out => .. y ..))

  while the choose may not directly reference x in its preducate, it's
  part of its path condition and should be usable by synthesis.
  SimplifyLet should not simplify/replace it.

- Modify PC for Let(x, Fcall()), this probably needs to be generalized!

- Expose counter-example found during verification, include them in
  VCReport

- Decouple genVCs/checkVCs from Phase.run so that it can be used separately

Normalizing rules are rules that:
1) always help synthesis
2) are commutative
3) should be applied as early as possible

Here we apply normalizing rules explicitly before all other rules, and
in a deterministic order. This should dramatically reduce the search
space in cases where such rules apply.

Note that rules that are said to be normalizing should never fail once
instantiated.

EqualitySplit now is also applied if there is more than two inputs with
the same type.

InequalitySplit splits two integer inputs in the following way:
- a < b
- a == b
- a > b

Given x: T where T only have one inhabitant, CC(a, b), we generate a
subproblem with a,b as out variables, and x replaced with CC(a,b) in phi

This allows CostModels to estimate correctly the minimal cost of a
applying a rule.

With type information on the expected types of a solution
reconstruction, the cost model can provide dummy values of the correct
type, avoiding assertion errors when composing solutions.

The synthesizer used to generate wrong programs by generating inductive
programs with an impossible base-case. onSuccess on inductive rules now
prevents this by checking that sufficiently many cases have precondition
== true. Otherwise, onSuccess fails. This last-moment failure is now
handled correctly.

Strenghten precondition

Handle problem of costs=0 in case of missing SolutionBuilder, requires passing more info to RuleInstantiation, but it is useful anyway

Note that many ADT problems seem to diverge now. Also, preconditions are
missing? Or maybe just not displayed.