--solvers=smt-cvc4-cex
--solvers=smt-cvc4-proof

Update scala-smtlib with support for parsing special DefFunsRec

Fixes a bug, where UnrollingSolver was interrupted but was not
stopping its internal solver, leading to a timeout not being
respected if the internal solver was stucked in a complicated
check operation. UnrollingSolver now takes a Solver with
Interruptible.

In order to do that, Leon now relies on a more recent version of
scala-smtlib, that provides a feature to kill the solver process
in a relatively clean way. Update the SMTLIBSolver code to
actually perform the kill operation on the interrupt.

reactivate tests for CVC4, if available. Remove non-linear testcase that
worked only on z3 (SumAndMax)

Update the build to reference the most recent version of
scala smt-lib and adapt the code to the new API.

Replace some use of NonStandardCommand by built-in standard
Commands of scala smt-lib.

 - Partial support for CVC4

- Implement smt and smt-z3/smt-cvc4 as options for --solvers

- Uses a main solver sources for verification/CLP, taking into account
  --solvers

- Implement Z3-SMT sets

- Add tests for Z3-SMT

- Implement the Leon Library in Leon-land rather than Scala-land.
  import leon.Utils._ becomes import leon.lang._
  import leon.Annotations._ becomes import leon.annontation._

  For now, the library defines generic Options and Lists.
  The library is automatically imported from the ./leon script, unless
  the --library=no option is passed.

- Support parsing of multiple files and modules.

- Introduce new annontations:
    @ignore: remove definition from Leon
    @verified: do not consider for verification unless explicitly
        specified

- 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

- 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

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.

sbt now generates two scripts,
  - ./leon
  - ./setupenv
setupenv needs to be evaluated before doing "sbt test". Make sure you
run it using "source ./setupenv" and not "./setupenv" so that the
exports contained in setupenv have an effect on the outer shell
context.

setupenv is used within ./leon as well

option is provided.