diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 0bacc4a72c160f7c04297c4e7a4d3153b36512d2..9fb28e66d21877d0ab88441d6fa586c684ea85ab 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/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._
 
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 48624c80952e521e8341bbd6df11343159e97b85..4fa399f7a2818799773b0698e7c717baaf5bd50f 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/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._
 
diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
index 7802d45093a5bc039c366cc6475bab24ef2ab2bb..60c2702485c3cdd55abab16e616dcca5d6952a80 100644
--- a/src/main/scala/leon/utils/PreprocessingPhase.scala
+++ b/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}
diff --git a/src/main/scala/leon/verification/GroupedTactic.scala b/src/main/scala/leon/verification/GroupedTactic.scala
index 4a551a2676feb0155953c3740812976afde9ccdd..02da7e55bc321cc79549922a409bc34364d91cfa 100644
--- a/src/main/scala/leon/verification/GroupedTactic.scala
+++ b/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 {