From b3157364090e015769f04dc0ced605454b089d64 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 26 May 2015 13:15:03 +0200
Subject: [PATCH] Change how postcond. are encoded in GroupedTactic
---
src/main/scala/leon/verification/GroupedTactic.scala | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/verification/GroupedTactic.scala b/src/main/scala/leon/verification/GroupedTactic.scala
index 6ef63a8f8..8bd957037 100644
--- a/src/main/scala/leon/verification/GroupedTactic.scala
+++ b/src/main/scala/leon/verification/GroupedTactic.scala
@@ -20,7 +20,9 @@ class GroupedTactic(vctx: VerificationContext) extends Tactic(vctx) {
} yield {
implies(
precOrTrue(inComp),
- application(p, Seq(b))
+ // @mk: Don't know which one is better. Inline the body, or have it as a fun. app?
+ //application(p, Seq(b))
+ application(p, Seq(FunctionInvocation(inComp.typedWithDef, inComp.params map { _.toVariable })))
)
}
--
GitLab