synchronized evaluator invariant cache & small fix in codegen

src/main/scala/leon/codegen/CompilationUnit.scala

@@ -213,9 +213,13 @@ class CompilationUnit(val ctx: LeonContext,
     case CaseClass(cct, args) =>
       caseClassConstructor(cct.classDef) match {
         case Some(cons) =>
-          val tpeParam = if (cct.tps.isEmpty) Seq() else Seq(cct.tps.map(registerType).toArray)
-          val jvmArgs = monitor +: (tpeParam ++ args.map(valueToJVM))
-          cons.newInstance(jvmArgs.toArray : _*).asInstanceOf[AnyRef]
+          try {
+            val tpeParam = if (cct.tps.isEmpty) Seq() else Seq(cct.tps.map(registerType).toArray)
+            val jvmArgs = monitor +: (tpeParam ++ args.map(valueToJVM))
+            cons.newInstance(jvmArgs.toArray : _*).asInstanceOf[AnyRef]
+          } catch {
+            case e : java.lang.reflect.InvocationTargetException => throw e.getCause
+          }
         case None =>
           ctx.reporter.fatalError("Case class constructor not found?!?")
       }

src/main/scala/leon/evaluators/Evaluator.scala

@@ -138,14 +138,15 @@ object Evaluator {
   case object Pending extends CheckStatus
   case object NoCheck extends CheckStatus
 
-  def invariantCheck(cc: CaseClass): CheckStatus =
+  def invariantCheck(cc: CaseClass): CheckStatus = synchronized {
     if (!cc.ct.classDef.hasInvariant) Complete(true)
     else checkCache.get(cc).getOrElse {
       checkCache(cc) = Pending
       NoCheck
     }
+  }
 
-  def invariantResult(cc: CaseClass, success: Boolean): Unit = {
+  def invariantResult(cc: CaseClass, success: Boolean): Unit = synchronized {
     checkCache(cc) = Complete(success)
   }