The reasonning is that when generating tests, we want  tests for when
the elements do not matter too much.

For instance, if we want tests for choose (x => x == a), and we only
have the test a = 0, then a+a will pass the test, 42 is less likely to
cause these.

- Refactor CEGIS options for clearer defaults

Allow more than 1 interrupts, exit if within 1 sec.
Register SMTLIB solvers for interrupt.