From d95757de1acf8a2f80a26748f1ad4bc3373d809e Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 4 Sep 2015 15:01:43 +0200
Subject: [PATCH] Give a position to artificial postc.
---
src/main/scala/leon/utils/TypingPhase.scala | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/utils/TypingPhase.scala b/src/main/scala/leon/utils/TypingPhase.scala
index 0f47e61ac..05648fc9f 100644
--- a/src/main/scala/leon/utils/TypingPhase.scala
+++ b/src/main/scala/leon/utils/TypingPhase.scala
@@ -61,7 +61,11 @@ object TypingPhase extends LeonPhase[Program, Program] {
).setPos(p)).setPos(p))
case None =>
- Some(Lambda(Seq(ValDef(resId)), IsInstanceOf(ct, Variable(resId))))
+ val pos = fd.body.map{ _.getPos } match {
+ case Some(df: DefinedPosition) => df.focusEnd
+ case _ => NoPosition
+ }
+ Some(Lambda(Seq(ValDef(resId)), IsInstanceOf(ct, Variable(resId))).setPos(pos))
}
}
case _ => fd.postcondition
--
GitLab