From a7ffa7c64058fd7b01b3568c0235543f0be06038 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 22 May 2015 12:34:41 +0200
Subject: [PATCH] We don't need to duplicate FunDef's when generating VCs
---
src/main/scala/leon/verification/Tactic.scala | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index 0571e3242..b424abf5f 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -10,8 +10,7 @@ import purescala.ExprOps._
abstract class Tactic(vctx: VerificationContext) {
val description : String
- def generateVCs(fdUnsafe: FunDef): Seq[VC] = {
- val fd = fdUnsafe.duplicate
+ def generateVCs(fd: FunDef): Seq[VC] = {
fd.fullBody = matchToIfThenElse(fd.fullBody)
generatePostconditions(fd) ++
generatePreconditions(fd) ++
--
GitLab