diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala index 366feffafcb9c7b994d6ccefbc1ff2f0269626dd..88f1679bceda88c4d535e2f5e51b18d7e5b1b1cb 100644 --- a/src/main/scala/leon/codegen/CompilationUnit.scala +++ b/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?!?") } diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala index 5ae1a57a6f5475c772b0fc950aac9bff7e5a76ea..c3d4c737f6d91492151b45c1acf99abf80574fda 100644 --- a/src/main/scala/leon/evaluators/Evaluator.scala +++ b/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) }