From 61f3a48bf49e6caa54653e5bc73a872b0e2531cb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 15 Apr 2016 20:17:43 +0200
Subject: [PATCH] epsilon functions generated with proper flags
---
src/main/scala/leon/xlang/EpsilonElimination.scala | 2 ++
1 file changed, 2 insertions(+)
diff --git a/src/main/scala/leon/xlang/EpsilonElimination.scala b/src/main/scala/leon/xlang/EpsilonElimination.scala
index 5ab872b84..4d77d89dd 100644
--- a/src/main/scala/leon/xlang/EpsilonElimination.scala
+++ b/src/main/scala/leon/xlang/EpsilonElimination.scala
@@ -30,6 +30,8 @@ object EpsilonElimination extends UnitPhase[Program] {
}.toMap ++ Seq((epsilonVar, Variable(resId)))
val postcondition = replace(eMap, pred)
newFunDef.postcondition = Some(Lambda(Seq(ValDef(resId)), postcondition))
+ newFunDef.addFlags(fd.flags)
+ newFunDef.addFlag(Annotation("extern", Seq()))
LetDef(Seq(newFunDef), FunctionInvocation(newFunDef.typed, bSeq map Variable))
case (other, _) => other
--
GitLab