Only generate one vc per function group in GroupedTactic

src/main/scala/leon/purescala/Extractors.scala

@@ -6,7 +6,6 @@ package purescala
 import Expressions._
 import Common._
 import Types._
-import Definitions._
 import Constructors._
 import ExprOps._
 

src/main/scala/leon/synthesis/Synthesizer.scala

@@ -10,7 +10,6 @@ import purescala.Expressions._
 import purescala.Constructors._
 import purescala.ScalaPrinter
 import solvers._
-import solvers.z3._
 
 import scala.concurrent.duration._
 

src/main/scala/leon/utils/PreprocessingPhase.scala

@@ -4,7 +4,6 @@ package leon
 package utils
 
 import purescala.Definitions.Program
-import purescala.ScalaPrinter
 
 import purescala.{MethodLifting, CompleteAbstractDefinitions,CheckADTFieldsTypes}
 import synthesis.{ConvertWithOracle, ConvertHoles}

src/main/scala/leon/verification/GroupedTactic.scala

@@ -3,6 +3,7 @@
 package leon
 package verification
 
+import leon.utils.NoPosition
 import purescala.Expressions._
 import purescala.ExprOps._
 import purescala.Definitions._
@@ -12,23 +13,28 @@ class GroupedTactic(vctx: VerificationContext) extends Tactic(vctx) {
     val description = "Default verification condition generation approach"
 
     def generatePostconditions(fd: FunDef): Seq[VC] = {
-      fd.postcondition map { post =>
-        val perFunc = for {
-          inComp <- vctx.program.callGraph.stronglyConnectedComponent(fd)
-          p <- inComp.postcondition
-          b <- inComp.body
-        } yield {
-          implies(
-            precOrTrue(inComp),
-            // @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 })))
-          )
-        }
-        
-        VC(andJoin(perFunc.toSeq), fd, VCKinds.Postcondition, this).setPos(post)
-      }
-    }.toSeq
+      // We collectively generate postconditions for a scc of the call graph.
+      // To not repeat vcs, we follow the convention to generate them for the first
+      // FunDef of the vcc according to unique name
+      val component = vctx.program.callGraph.stronglyConnectedComponent(fd).toSeq sortBy (_.id.uniqueName)
+      val perFunc:Seq[Expr] = for {
+        generator <- component.find( _.postcondition.isDefined).toSeq
+        if generator == fd
+        inComp <- component
+        p <- inComp.postcondition
+        b <- inComp.body
+      } yield { implies(
+        precOrTrue(inComp),
+        // @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 })))
+      )}
+
+      if (perFunc.nonEmpty)
+        Seq(VC(andJoin(perFunc.toSeq), fd, VCKinds.Postcondition, this).setPos(fd.postcondition.get))
+      else Nil
+
+    }
 
     def generatePreconditions(fd: FunDef): Seq[VC] = {
       fd.body match {