diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 3e848994835d9e8bc6a4506576ede13439c0664b..45c62bd0d3a5e82735b98237d2671f485915d13d 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -21,7 +21,7 @@ object Main {
       purescala.FunctionClosure,
       synthesis.SynthesisPhase,
       termination.TerminationPhase,
-      verification.AnalysisPhase,
+      verification.VerificationPhase,
       repair.RepairPhase,
       evaluators.EvaluationPhase,
       solvers.isabelle.AdaptationPhase,
@@ -147,7 +147,7 @@ object Main {
     import synthesis.SynthesisPhase
     import termination.TerminationPhase
     import xlang.FixReportLabels
-    import verification.AnalysisPhase
+    import verification.VerificationPhase
     import repair.RepairPhase
     import evaluators.EvaluationPhase
     import solvers.isabelle.IsabellePhase
@@ -177,19 +177,19 @@ object Main {
         ExtractionPhase andThen
         new PreprocessingPhase(xlangF)
 
-      val analysis = if (xlangF) AnalysisPhase andThen FixReportLabels else AnalysisPhase
+      val verification = if (xlangF) VerificationPhase andThen FixReportLabels else VerificationPhase
 
       val pipeProcess: Pipeline[Program, Any] = {
         if (noopF) RestoreMethods andThen FileOutputPhase
         else if (synthesisF) SynthesisPhase
         else if (repairF) RepairPhase
-        else if (analysisF) Pipeline.both(analysis, TerminationPhase)
+        else if (analysisF) Pipeline.both(verification, TerminationPhase)
         else if (terminationF) TerminationPhase
         else if (isabelleF) IsabellePhase
         else if (evalF) EvaluationPhase
         else if (inferInvF) InferInvariantsPhase
         else if (instrumentF) InstrumentationPhase andThen FileOutputPhase
-        else analysis
+        else verification
       }
 
       pipeBegin andThen
diff --git a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
index ce69f2b6f755279d333471bacf9aa0579013defd..4bc1e245fe8de74c8c6a4c048164e5583c00adba 100644
--- a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
+++ b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
@@ -144,7 +144,7 @@ object InferInvariantsPhase extends SimpleLeonPhase[Program, InferenceReport] {
   }
 
   def validateAndCollectNotValidated(prog: Program, ctx: LeonContext, timeout: Int): Set[String] = {
-    val verifyPipe = AnalysisPhase
+    val verifyPipe = VerificationPhase
     val ctxWithTO = createLeonContext(ctx, "--timeout=" + timeout)
     (verifyPipe.run(ctxWithTO, prog)._2).results.collect{
       case (VC(_, fd, VCKinds.Postcondition), Some(vcRes)) if vcRes.isInconclusive =>
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index aac4a8d4a98bfde48f786785b4388392f762953c..1f939c96e9ca70c72c22fac6f1b8378864b6458f 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -167,10 +167,10 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
     val timeoutMs = verifTimeoutMs.getOrElse(3000L)
     val solverf = SolverFactory.getFromSettings(ctx, program).withTimeout(timeoutMs)
     val vctx = VerificationContext(ctx, program, solverf, reporter)
-    val vcs = AnalysisPhase.generateVCs(vctx, Seq(fd))
+    val vcs = VerificationPhase.generateVCs(vctx, Seq(fd))
 
     try {
-      val report = AnalysisPhase.checkVCs(
+      val report = VerificationPhase.checkVCs(
         vctx,
         vcs,
         stopAfter = Some({ (vc, vr) => vr.isInvalid })
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 7ed4d56a8a74e5a16301026ff2328ba8243d8716..54e305adf11ebc9314c262b4be5b203df8337771 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -70,7 +70,7 @@ class Synthesizer(val context : LeonContext,
   }
 
   def validateSolution(search: Search, sol: Solution, timeout: Duration): (Solution, Boolean) = {
-    import verification.AnalysisPhase._
+    import verification.VerificationPhase._
     import verification.VerificationContext
 
     reporter.info("Solution requires validation")
diff --git a/src/main/scala/leon/verification/VerificationContext.scala b/src/main/scala/leon/verification/VerificationContext.scala
index ba3b5024e27ea34da381f1cf148e8b9d096e73a4..2aaa910ab6450c0de300e36ec42ad71d7b073d84 100644
--- a/src/main/scala/leon/verification/VerificationContext.scala
+++ b/src/main/scala/leon/verification/VerificationContext.scala
@@ -12,5 +12,5 @@ case class VerificationContext (
   solverFactory: SolverFactory[Solver],
   reporter: Reporter
 ) {
-  val checkInParallel: Boolean = context.findOptionOrDefault(AnalysisPhase.optParallelVCs)
+  val checkInParallel: Boolean = context.findOptionOrDefault(VerificationPhase.optParallelVCs)
 }
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/VerificationPhase.scala
similarity index 96%
rename from src/main/scala/leon/verification/AnalysisPhase.scala
rename to src/main/scala/leon/verification/VerificationPhase.scala
index e5edc13084cc1bd372b6e67254caebaab7e9134f..21119c4e2728c99850e3af0d1c12e498866f771e 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/VerificationPhase.scala
@@ -11,9 +11,9 @@ import java.lang.System
 
 import solvers._
 
-object AnalysisPhase extends SimpleLeonPhase[Program,VerificationReport] {
-  val name = "Analysis"
-  val description = "Leon Verification"
+object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] {
+  val name = "Verification"
+  val description = "Verification of function contracts"
 
   val optParallelVCs = LeonFlagOptionDef("parallel", "Check verification conditions in parallel", default = false)
 
diff --git a/src/test/scala/leon/regression/repair/RepairSuite.scala b/src/test/scala/leon/regression/repair/RepairSuite.scala
index 2ac93521b9acb07996fbf52ca0158070811ca237..50b845f923e2356d1ce4c0c9a27692a78cd30ce5 100644
--- a/src/test/scala/leon/regression/repair/RepairSuite.scala
+++ b/src/test/scala/leon/regression/repair/RepairSuite.scala
@@ -7,7 +7,7 @@ import leon.test._
 import leon.utils._
 import leon.frontends.scalac.ExtractionPhase
 import leon.repair._
-import leon.verification.AnalysisPhase
+import leon.verification.VerificationPhase
 
 class RepairSuite extends LeonRegressionSuite {
   val pipeline = ExtractionPhase andThen 
@@ -35,7 +35,7 @@ class RepairSuite extends LeonRegressionSuite {
       interruptManager = new InterruptManager(reporter),
       options = Seq(
         LeonOption(SharedOptions.optFunctions)(Seq(fileToFun(name))),
-        LeonOption(AnalysisPhase.optParallelVCs)(true),
+        LeonOption(VerificationPhase.optParallelVCs)(true),
         LeonOption(SharedOptions.optTimeout)(180L)
       )
     )
diff --git a/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala b/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala
index bd44226988a11516cfadb4eec35174972662d263..d350bd04b4c68f7838676048b47b085b5d54e4b8 100644
--- a/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala
@@ -6,13 +6,13 @@ import leon._
 import leon.test._
 import leon.frontends.scalac.ExtractionPhase
 import leon.utils.PreprocessingPhase
-import leon.verification.AnalysisPhase
+import leon.verification.VerificationPhase
 
 class LibraryVerificationSuite extends LeonRegressionSuite {
   test("Verify the library") {
       val pipeline = ExtractionPhase    andThen
                      new PreprocessingPhase andThen
-                     AnalysisPhase
+                     VerificationPhase
 
       val ctx = Main.processOptions(Seq("--functions=_")).copy(reporter = new TestSilentReporter())
 
diff --git a/src/test/scala/leon/regression/verification/NewSolversSuite.scala b/src/test/scala/leon/regression/verification/NewSolversSuite.scala
index 6eac7183e9244661e024fdaa9f9cc770c16f7768..6065d8232341060f0f0eeae735961ae8c5e73da3 100644
--- a/src/test/scala/leon/regression/verification/NewSolversSuite.scala
+++ b/src/test/scala/leon/regression/verification/NewSolversSuite.scala
@@ -4,7 +4,7 @@ package leon.regression.verification
 
 import _root_.smtlib.interpreters._
 import leon._
-import leon.verification.AnalysisPhase
+import leon.verification.VerificationPhase
 
 /* @EK: Disabled for now as many tests fail 
 class NewSolversSuite extends VerificationSuite {
diff --git a/src/test/scala/leon/regression/verification/VerificationSuite.scala b/src/test/scala/leon/regression/verification/VerificationSuite.scala
index 06b00e0bb2748acb86ff9209ed1c8a1d45d53d18..b23fb0c4e3516121a1489752ed89dcb0835ee2d2 100644
--- a/src/test/scala/leon/regression/verification/VerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/VerificationSuite.scala
@@ -6,7 +6,7 @@ import leon._
 import leon.test._
 
 import leon.utils.UniqueCounter
-import leon.verification.{AnalysisPhase, VerificationReport}
+import leon.verification.{VerificationPhase, VerificationReport}
 import leon.purescala.Definitions.Program
 import leon.frontends.scalac.ExtractionPhase
 import leon.utils.PreprocessingPhase
@@ -38,7 +38,7 @@ trait VerificationSuite extends LeonRegressionSuite {
 
     val analysis =
       (if (isabelle) AdaptationPhase else NoopPhase[Program]) andThen
-      AnalysisPhase andThen
+      VerificationPhase andThen
       (if (desugarXLang) FixReportLabels else NoopPhase[VerificationReport])
 
     val ctx = createLeonContext(files:_*)