Solvers wrap solvers or factories, depending on the needs.
Factories no longer wrap factories, except for the special case of
timeoutsolverfactories (it does it in a typesafe way though).

Fix TupleRewrite with new posts, fix ScopeSimplified, Fix pretty printer

- RewritingSolver
- DNFSolver
- UnrollingSolver

Refactored the condition abduction code, refactored InSynth code out of Leon, and added the InSynth core library, with substantial amount of fixing and clearning sources, tests, and testcases

Refactoring and fixes for compliance with the rule framework (huge commit and subsequent fixes in the oopsla-artifact branch)

Refactored verifier into concrete and timeout one, added generation of input examples with fuzzying, expression filter detects according to expression structure, added some benchmarks for the paper

Changed the verification condition generation, mofidified filtered of candidates, implemented verifier timeout as evidence of validity

Changed checking for counterexample implications from verification to evaluation, added evaluation strategies (default and codegen), some heuristics, measurements

Added added necessary sources and tests for insynth and condition abduction, and two synthesis rules (immediate and deferred instantiation)

Unlocking reused, already-unlocked blockers would result in a no-op
while still keeping this blocker into the list of blockers to address.
This patch makes sure that reused, unlocked blockers are excluded from
the worklist.

This should prevent false-negatives on unpredictably slow veficiation
tests such as invalid/RedBlackTree.

- 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

- We now explicitly create them from SolverFactories
- SolveSAT/solve/solveWithModel/etc.. is not only available through the
  SimpleSolverAPI() wrapper.o
- Remove mostly unused/useless solvers

For now only synthesis tests that 100% pass. The rest of benchmarks need
to be investigated due to memory consumption issues

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.