Fix potential infinite loop with unlocking of reused blockers

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.
Relax the way we report slow tests. Enforce types on set operations
Added added necessary sources and tests for insynth and condition abduction, and two synthesis rules (immediate and deferred instantiation)
Changes before the submission - DataGen, benchmarks, timeout checking
Added support for candidate ranking (for minimizing #evaluations)
More flexible variable refinement - direct field refinement, operator refinement
Changed checking for counterexample implications from verification to evaluation, added evaluation strategies (default and codegen), some heuristics, measurements
Changed the verification condition generation, mofidified filtered of candidates, implemented verifier timeout as evidence of validity
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
Refactoring and fixes for compliance with the rule framework (huge commit and subsequent fixes in the oopsla-artifact branch)
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
Moved code to appropriate packages and formatted sources
Remove unused file, fix style
First step to bring everything about Lemmas out of FairZ3Solver class :)
Clean the mess of code by extending FairZ3Solver class instead of changing original class
Clean Analysis phase with new extended class
Fix some mistakes, hope it okay okay with travis testing right now
Once again, I don't that I have to change other stuff to test regression works with new Analisys phase, anw, everything is okay right now :-)
Merge remote-tracking branch 'lara-leon/master' into simp-tactic
Now simp-tactic with new code structure from branch XNgin