diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala index 5ada9b2235518e8fe7a3cc49e329392813c0eb86..67071a6d00e240bcd731e57227c4d627572e2357 100644 --- a/src/main/scala/leon/plugin/CodeExtraction.scala +++ b/src/main/scala/leon/plugin/CodeExtraction.scala @@ -534,8 +534,8 @@ trait CodeExtraction extends Extractors { val tupleType = TupleType(tupleExprs.map(expr => bestRealType(expr.getType))) Tuple(tupleExprs).setType(tupleType) } - case ExErrorExpression(str) => - Error(str).setType(scalaType2PureScala(unit, silent)(nextExpr.tpe)) + case ExErrorExpression(str, tpe) => + Error(str).setType(scalaType2PureScala(unit, silent)(tpe)) case ExTupleExtract(tuple, index) => { val tupleExpr = rec(tuple) diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala index e736f75368e3bede82826bb3fab346d7fc43d9ff..8b3eebd4b27da35614412acaad96428477311278 100644 --- a/src/main/scala/leon/plugin/Extractors.scala +++ b/src/main/scala/leon/plugin/Extractors.scala @@ -183,9 +183,9 @@ trait Extractors { } object ExErrorExpression { - def unapply(tree: Apply) : Option[String] = tree match { - case a @ Apply(Select(Select(Select(ExIdNamed("scala"), ExNamed("sys")), ExNamed("package")), ExNamed("error")), List(lit : Literal)) => - Some(lit.value.stringValue) + def unapply(tree: Apply) : Option[(String, Type)] = tree match { + case a @ Apply(TypeApply(Select(Select(ExIdNamed("leon"), ExNamed("Utils")), ExNamed("error")), List(tpe)), List(lit : Literal)) => + Some((lit.value.stringValue, tpe.tpe)) case _ => None } diff --git a/testcases/Errors.scala b/testcases/Errors.scala new file mode 100644 index 0000000000000000000000000000000000000000..b6d7dc74e5ba82ebac0863fd411e4b00ef475bc7 --- /dev/null +++ b/testcases/Errors.scala @@ -0,0 +1,6 @@ +import leon.Utils._ + +object Errors { + def a(a: Int): Int = error[Int]("This is an error") +} +