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.

- Debug sections can be toggled to enable detailled information
- Options can be explicitly turned off, --debug:options lists all
- Switch from multiple reporters to a single one to rule them all
- Turn cegis:gencalls on by default

- Search tree can be iterated over in order
- Worker pool get displayed periodically when stuck
- Make sure global caches are concurrent