It used to be extremely bad: if the interesting failing test is the last
one (of 300), CEGISLike would test 1000*300 times before ordering it to
make it first.

Now we assume that interesting tests are discovered early.

Fixing canBeSubtypeOf caused List1 to become too hard due to slowness in
testing the large grammar. Temporarily fixing tests until we find a
decent solution.

Solvers are no longer distinguished in 20 traits depending on what they
implement. It turns out that most leon solvers already implemented
everything:

1) Being interrupted
2) Push / Pop
3) checkAssertions/getUnsatCore (a naive implementation of these
   can be added by mixing NaiveAssumptionSolver in)