CEGIS now support internal flags that can enable/disable its features:

1) Injecting Counter-Examples on top of the unsat core to drive the
   search to interesting areas. Does not help => disabled

2) Computing Unsat-Cores to strenghten the search of programs. Help in
   some cases, doesn't hurt much => enabled

3) Checking whether the formula is unsat without blockers, to unrolling
   when there is no chance of finding a solution. Does not help =>
   disable

4) Add support for function calls in CEGIS generators. This is disabled
   by default and can be enabled using --cegis:gencalls.

It seems that doing additional checks in 1) and 3) triggers FairZ3 to
unroll more, tempering with the performance of the solver.

Also, this implements some improvements in the resulting programs by
simplifying further expressions.