Remove old VC gen (#1347)

.larabot.conf

@@ -1,6 +1,6 @@
 commands = [
     "sbt -batch -Dtest-parallelism=5 test"
-    "sbt -batch -Dtest-parallelism=5 \"it:testOnly stainless.GhostRewriteSuite stainless.GenCSuite stainless.TypeCheckerLibrarySuite stainless.ScalacExtractionSuite stainless.LibrarySuite stainless.verification.SMTZ3TypeCheckerSuite stainless.verification.SMTZ3VerificationSuite stainless.verification.SMTZ3UncheckedSuite stainless.verification.TerminationVerificationSuite stainless.verification.ImperativeSuite stainless.verification.FullImperativeSuite stainless.verification.StrictArithmeticSuite stainless.verification.CodeGenVerificationSuite stainless.verification.SMTCVC4TypeCheckerSuite stainless.verification.SMTCVC4VerificationSuite stainless.verificatoin.SMTCVC4UncheckedSuite stainless.termination.TerminationSuite\""
+    "sbt -batch -Dtest-parallelism=5 \"it:testOnly stainless.GhostRewriteSuite stainless.GenCSuite stainless.ScalacExtractionSuite stainless.LibrarySuite stainless.verification.SMTZ3VerificationSuite stainless.verification.SMTZ3UncheckedSuite stainless.verification.TerminationVerificationSuite stainless.verification.ImperativeSuite stainless.verification.FullImperativeSuite stainless.verification.StrictArithmeticSuite stainless.verification.CodeGenVerificationSuite stainless.verification.SMTCVC4VerificationSuite stainless.verificatoin.SMTCVC4UncheckedSuite stainless.termination.TerminationSuite\""
 ]
 
 nightly {

core/src/main/scala/stainless/MainHelpers.scala

@@ -51,7 +51,6 @@ trait MainHelpers extends inox.MainHelpers { self =>
     verification.optAdmitAll -> Description(Verification, "Admit all obligations when translated into a coq program"),
     verification.optStrictArithmetic -> Description(Verification,
       s"Check arithmetic operations for unintended behavior and overflows (default: true)"),
-    verification.optTypeChecker -> Description(Verification, "Use the type-checking rules from the calculus to generate verification conditions"),
     verification.optAdmitVCs -> Description(Verification, "Admit all verification conditions"),
     verification.optSimplifier -> Description(Verification, "Select which simplifier to use for VC simplification\n" +
       "Available:\n" +

core/src/main/scala/stainless/Report.scala

@@ -173,15 +173,13 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
     val sd = prepareExtractionSummaryData
     val admitted = ctx.options.findOptionOrDefault(verification.optAdmitVCs)
     val termOff = ctx.options.findOptionOrDefault(stainless.termination.optCheckMeasures).isNo
-    val oldVC = !ctx.options.findOptionOrDefault(verification.optTypeChecker)
     val cache = ctx.options.findOptionOrDefault(verification.optVCCache)
     val solvers = ctx.options.findOptionOrDefault(inox.optSelectedSolvers).toSeq.sorted.mkString(", ")
     val batched = ctx.options.findOptionOrDefault(frontend.optBatchedProgram)
 
     if (isExtendedSummaryOn) {
       val admitStr = if (admitted) withColor("Admitted VCs", Console.RED, Console.BOLD) else ""
       val termOffStr = if (termOff) withColor("Termination turned off", Console.RED, Console.BOLD) else ""
-      val oldVCStr = if (oldVC) withColor("Old VCs generation", Console.RED, Console.BOLD) else ""
       val cacheStr = if (cache) "Cache used" else ""
 
       def touched(sentance: String, ids: Set[Identifier], prefix: String): String =
@@ -216,13 +214,12 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
       val solversUsed = s"Solvers used: $solvers"
       val procMode = s"Processing mode: ${if (batched) "batched" else "partial"}"
 
-      val items = Seq(admitStr, termOffStr, oldVCStr, cacheStr, aaStr, reStr, weStr, ieStr, teStr, ceStr, solversUsed, procMode).filter(_.nonEmpty)
+      val items = Seq(admitStr, termOffStr, cacheStr, aaStr, reStr, weStr, ieStr, teStr, ceStr, solversUsed, procMode).filter(_.nonEmpty)
       s"""Verification pipeline summary:
          |${items.mkString("  ", "\n  ", "")}""".stripMargin // No join(items) here as their sub-items are already split according to the character limit
     } else {
       val admitStr = if (admitted) withColor("admitted VCs", Console.RED, Console.BOLD) else ""
       val termOffStr = if (termOff) withColor("termination off", Console.RED, Console.BOLD) else ""
-      val oldVCStr = if (oldVC) withColor("old VCs gen", Console.RED, Console.BOLD) else ""
       val cacheStr = if (cache) "cache" else ""
       val aaStr = if (sd.antiAliasing.hasRun) "anti-aliasing" else ""
       val reStr = if (sd.retAndWhileTran.hasReturnRun) "return transformation" else ""
@@ -231,7 +228,7 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
       val teStr = if (sd.typeEncoding.hasRun) "type encoding" else ""
       val ceStr = if (sd.chooseInjection.hasRun) withColor("choose injection", Console.YELLOW, Console.BOLD) else ""
       val batchedStr = if (batched) "batched" else ""
-      val items = Seq(admitStr, termOffStr, oldVCStr, cacheStr, aaStr, reStr, weStr, ieStr, teStr, ceStr, solvers, batchedStr).filter(_.nonEmpty)
+      val items = Seq(admitStr, termOffStr, cacheStr, aaStr, reStr, weStr, ieStr, teStr, ceStr, solvers, batchedStr).filter(_.nonEmpty)
       s"""Verification pipeline summary:
          |${join(items, prefix = "  ")}""".stripMargin
     }

core/src/main/scala/stainless/verification/VerificationComponent.scala

@@ -18,11 +18,6 @@ import stainless.termination.MeasureInference
  */
 object optStrictArithmetic extends inox.FlagOptionDef("strict-arithmetic", true)
 
-/**
- * Generate VC via the System FR type-checker instead of the ad-hoc DefaultTactic.
- */
-object optTypeChecker extends inox.FlagOptionDef("type-checker", true)
-
 /**
  * Verify program using Coq
  */
@@ -106,13 +101,8 @@ class VerificationRun private(override val component: VerificationComponent.type
 
       val vcGenEncoder = assertionEncoder
 
-      val vcs = if (context.options.findOptionOrDefault(optTypeChecker))
-        context.timers.verification.get("type-checker").run {
-          TypeChecker(vcGenEncoder.targetProgram, context).checkFunctionsAndADTs(functions)
-        }
-      else {
-        reporter.warning("Old VC generation is deprecated and scheduled for removal in 1.0")
-        VerificationGenerator.gen(vcGenEncoder.targetProgram, context)(functions)
+      val vcs = context.timers.verification.get("type-checker").run {
+        TypeChecker(vcGenEncoder.targetProgram, context).checkFunctionsAndADTs(functions)
       }
 
       if (!functions.isEmpty) {

frontends/common/src/it/scala/stainless/ComponentTestSuite.scala

@@ -17,7 +17,6 @@ trait ComponentTestSuite extends inox.TestSuite with inox.ResourceUtils with Inp
 
   override def configurations: Seq[Seq[inox.OptionValue[_]]] = Seq(
     Seq(
-      verification.optTypeChecker(true),
       inox.optSelectedSolvers(Set("smt-z3:z3-4.8.12")),
       inox.optTimeout(300.seconds),
       verification.optStrictArithmetic(false),
@@ -31,8 +30,7 @@ trait ComponentTestSuite extends inox.TestSuite with inox.ResourceUtils with Inp
   override protected def optionsString(options: inox.Options): String = {
     "solvr=" + options.findOptionOrDefault(inox.optSelectedSolvers).head + " " +
     "lucky=" + options.findOptionOrDefault(inox.solvers.unrolling.optFeelingLucky) + " " +
-    "check=" + options.findOptionOrDefault(inox.solvers.optCheckModels) + " "
-    "type-checker=" + options.findOptionOrDefault(verification.optTypeChecker)
+    "check=" + options.findOptionOrDefault(inox.solvers.optCheckModels)
   }
 
   protected def filter(ctx: inox.Context, name: String): FilterStatus = Test

frontends/common/src/it/scala/stainless/LibrarySuite.scala

@@ -56,11 +56,6 @@ abstract class AbstractLibrarySuite(opts: Seq[inox.OptionValue[_]]) extends AnyF
 }
 
 class LibrarySuite extends AbstractLibrarySuite(Seq(
-  verification.optTypeChecker(false)
-))
-
-class TypeCheckerLibrarySuite extends AbstractLibrarySuite(Seq(
-  verification.optTypeChecker(true),
   termination.optInferMeasures(true),
   termination.optCheckMeasures(YesNoOnly.Yes),
 ))

frontends/common/src/it/scala/stainless/termination/TerminationSuite.scala

@@ -16,7 +16,6 @@ class TerminationSuite extends VerificationComponentTestSuite {
 
   override def configurations = super.configurations.map { seq =>
     Seq(
-      optTypeChecker(true),
       optInferMeasures(true),
       optCheckMeasures(YesNoOnly.Only),
     ) ++ seq

frontends/common/src/it/scala/stainless/verification/TerminationVerificationSuite.scala

@@ -10,7 +10,6 @@ class TerminationVerificationSuite extends VerificationComponentTestSuite {
   override def configurations = super.configurations.map { seq =>
     Seq(
       optFailInvalid(true),
-      verification.optTypeChecker(true),
       termination.optInferMeasures(false),
       termination.optCheckMeasures(YesNoOnly.No),
     ) ++ seq