Use WeakHashMap/WeakReference to ensure that
1) ChooseEntryPoint does not prevent collection of CompilationUnit
2) Whenever CompilationUnit is collected, ChooseId become collectable

This fixes a huge memory leak in Leon's runtime constraint solving.

> @ignore
> implicit class Foo(x: ..)

generates an implicit synthetic conversion without @ignore. We
explicitly ignore these as they are extracted specially. However, we
should *not* ignore implicit defs that the user defined for convenience.

Sadly, Scala does not support "implicit case class", so in Leon
you have to use a normal case class with a normal implicit conversion
that wraps in the case-class:

> case class Foo(x: Bar)
> implicit def barToFoo(b: Bar): Foo = Foo(b)

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.