CE-Testing allows CEGIS to compile the program at the current unrolling
level and test with provided Bs (the determinized program) on previously
discovered inputs. This allows us to skip a SAT query in case one of
them fails.

Given a series of known valid inputs, it can prune program candidates by
enumerating them and testing against these inputs. This should
dramatically reduce the number of SAT queries. Currently we have no
heuristic to disable enumarting when branching factor becomes too big.
We might want to do random sampling.

We start by figuring out one basic examples that we can use for pruning.
In the presence of a path-condition, we need to perform a simple SAT
query

Also, B-Paths enforces sub-branches to use a fixed value if the parent
branch is closed. This should prune the program exploration behind
closed branches. We have observed no clear benefits in terms of
performance yet.

CEGIS will only use fully determined functions as candidates for
gencalls. (e.g. no functions containing 'choose')