--solvers=smt-cvc4-cex
--solvers=smt-cvc4-proof

Update scala-smtlib with support for parsing special DefFunsRec

In order to have support for maps, you need to import leon.lang._

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)