From b453606df950a3938bec302b228237f7febfb7c0 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 4 Mar 2015 20:13:07 +0100
Subject: [PATCH] Make sure we call application constructor
---
src/main/scala/leon/purescala/Extractors.scala | 2 +-
src/main/scala/leon/verification/DefaultTactic.scala | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index ce0535337..3ec5fcf2a 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -106,7 +106,7 @@ object Extractors {
}))
case fi @ FunctionInvocation(fd, args) => Some((args, (as => FunctionInvocation(fd, as).setPos(fi))))
case mi @ MethodInvocation(rec, cd, tfd, args) => Some((rec +: args, (as => MethodInvocation(as.head, cd, tfd, as.tail).setPos(mi))))
- case fa @ Application(caller, args) => Some((caller +: args), (as => Application(as.head, as.tail).setPos(fa)))
+ case fa @ Application(caller, args) => Some((caller +: args), (as => application(as.head, as.tail).setPos(fa)))
case CaseClass(cd, args) => Some((args, CaseClass(cd, _)))
case And(args) => Some((args, and))
case Or(args) => Some((args, or))
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 665cf21f0..6ecd9f720 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -69,7 +69,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
(a, kind, cond)
case a @ Assert(cond, None, _) => (a, VCAssert, cond)
// Only triggered for inner ensurings, general postconditions are handled by generatePostconditions
- case a @ Ensuring(body, post) => (a, VCAssert, Application(post, Seq(body)))
+ case a @ Ensuring(body, post) => (a, VCAssert, application(post, Seq(body)))
}(body)
calls.map {
--
GitLab