diff --git a/library/src/main/scala/leon/Utils.scala b/library/src/main/scala/leon/Utils.scala index a6d1ea771b7ec9df0fdb0be54eab5216650f1b0e..366cc39750b9779ebb1637f88b12bf9f86936fb4 100644 --- a/library/src/main/scala/leon/Utils.scala +++ b/library/src/main/scala/leon/Utils.scala @@ -27,4 +27,6 @@ object Utils { def choose[A, B, C](predicate: (A, B, C) => Boolean): (A, B, C) = noChoose def choose[A, B, C, D](predicate: (A, B, C, D) => Boolean): (A, B, C, D) = noChoose def choose[A, B, C, D, E](predicate: (A, B, C, D, E) => Boolean): (A, B, C, D, E) = noChoose + + def error[T](reason: String): T = sys.error(reason) } diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala index fb1e147857944acfdfcd93f0ddffc81faa2cbcc8..feff130eec0fc5b82068a9cc46908d571fcc1670 100644 --- a/src/main/scala/leon/purescala/ScalaPrinter.scala +++ b/src/main/scala/leon/purescala/ScalaPrinter.scala @@ -426,7 +426,9 @@ object ScalaPrinter { case e @ Error(desc) => { var nsb = sb - nsb.append("sys.error(\"" + desc + "\")") + nsb.append("leon.Utils.error[") + nsb = pp(e.getType, nsb, lvl) + nsb.append("](\"" + desc + "\")") nsb }