- 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

Ensures that tests run in an acceptable amount of time.
Needs at least 5 runs. Can cause failures of test-only due to
warm-up and class loading effects.

Improve performance of FairZ3 by lowering unrolling to the z3 level.  Improve synthesis profiling script.

Improve performance of FairZ3:

  Make function templates and unlocking/unrolling work directly at the z3 level for performance reasons.

  Implement push-pop at the unrolling-bank level. Works around a z3 bug.

  Z3 apparently side-effects during check-assumptions, causing a following
  check without assumptions to produce unreliable results. We work around this
  by backtracking to the state before the check-assumptions using
  push/pop.

Improve synthesis profiling/benchmarking:

  Move benchrmarking suite away from tests. Synthesis Rule application
  benchmark can now use a --rule option specifying what rule to apply.

  Add Testcase to evaluate CEGIS unrolling of different depth.
  Benchmarking script is now generated via the 'bench' sbt task.