Remove ImplPrivateInlining and @implPrivate (no longer needed)

core/src/main/scala/stainless/ast/Deconstructors.scala

@@ -226,7 +226,6 @@ trait TreeDeconstructor extends inox.ast.TreeDeconstructor {
     case s.PartialEval => (Seq(), Seq(), Seq(), (_, _, _) => t.PartialEval)
     case s.Wrapping => (Seq(), Seq(), Seq(), (_, _, _) => t.Wrapping)
     case s.Template => (Seq(), Seq(), Seq(), (_, _, _) => t.Template)
-    case s.ImplPrivate => (Seq(), Seq(), Seq(), (_, _, _) => t.ImplPrivate)
     case s.TerminationStatus(status) => (Seq(), Seq(), Seq(), (_, _, _) => t.TerminationStatus(status))
     case _ => super.deconstruct(f)
   }

core/src/main/scala/stainless/ast/Definitions.scala

@@ -29,7 +29,6 @@ trait Definitions extends inox.ast.Definitions { self: Trees =>
   case object PartialEval extends Flag("partialEval", Seq())
   case object Wrapping extends Flag("wrapping", Seq.empty)
   case object Template extends Flag("template", Seq.empty)
-  case object ImplPrivate extends Flag("implPrivate", Seq.empty)
 
   case class Derived(idOpt: Option[Identifier]) extends Flag("derived", idOpt.toSeq)
   case class IsField(isLazy: Boolean) extends Flag("field", Seq.empty)
@@ -53,7 +52,6 @@ trait Definitions extends inox.ast.Definitions { self: Trees =>
     case ("wrapping", Seq()) => Wrapping
     case ("template", Seq()) => Template
     case ("inlineInvariant", Seq()) => InlineInvariant
-    case ("implPrivate", Seq()) => ImplPrivate
     case _ => Annotation(name, args)
   }
 

core/src/main/scala/stainless/extraction/package.scala

@@ -59,7 +59,6 @@ package object extraction {
     "MeasureInference"          -> "Infer and inject measures in recursive functions",
     "PartialEvaluation"         -> "Partially evaluate marked function calls",
     "AssertionInjector"         -> "Insert assertions which verify array accesses, casts, division by zero, etc.",
-    "ImplPrivateInlining"       -> "Inline @implPrivate functions ahead of VC generation",
     "ChooseInjector"            -> "Insert chooses where necessary",
 
     "ComputeDependencies"       -> "(GenC) Compute the dependencies of a given definition",

core/src/main/scala/stainless/solvers/InoxEncoder.scala

@@ -20,8 +20,7 @@ trait InoxEncoder extends ProgramEncoder {
   private[this] def keepFlag(flag: Flag): Boolean = flag match {
     case DropVCs | DropConjunct | Library | Synthetic | PartialEval | Extern => false
     case Opaque | Private | Final | Law | Ghost | Erasable | Wrapping | Lazy => false
-    case Derived(_) | IsField(_) | IsUnapply(_, _) | IndexedAt(_) | ClassParamInit(_) |
-         ImplPrivate => false
+    case Derived(_) | IsField(_) | IsUnapply(_, _) | IndexedAt(_) | ClassParamInit(_) => false
     case TerminationStatus(_) => false
     case InlineInvariant | Template => false
     case _ => true

core/src/main/scala/stainless/utils/Serialization.scala

@@ -19,9 +19,9 @@ class StainlessSerializer(override val trees: ast.Trees, serializeProducts: Bool
   /** An extension to the set of registered classes in the `InoxSerializer`.
     * occur within Stainless programs.
     *
-    * The new identifiers in the mapping range from 120 to 172.
+    * The new identifiers in the mapping range from 120 to 171.
     *
-    * NEXT ID: 173
+    * NEXT ID: 172
     */
   override protected def classSerializers: Map[Class[_], Serializer[_]] =
     super.classSerializers ++ Map(
@@ -88,7 +88,6 @@ class StainlessSerializer(override val trees: ast.Trees, serializeProducts: Bool
       classSerializer[InlineInvariant.type](166),
       classSerializer[Lazy.type]       (167),
       classSerializer[Template.type]   (169),
-      classSerializer[ImplPrivate.type](172),
     )
 }
 

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

@@ -75,13 +75,6 @@ class VerificationRun(override val pipeline: StainlessPipeline)
     val t: self.trees.type = self.trees
   }
 
-  private[this] val debugImplPrivateInlining = new DebugSymbols {
-    val name = "ImplPrivateInlining"
-    val context = self.context
-    val s: self.trees.type = self.trees
-    val t: self.trees.type = self.trees
-  }
-
   private[this] val debugChooses = new DebugSymbols {
     val name = "ChooseInjector"
     val context = self.context
@@ -100,18 +93,9 @@ class VerificationRun(override val pipeline: StainlessPipeline)
 
       val assertions = AssertionInjector(p, context)
       val chooses = ChooseInjector(p)
-      val implPrivateInlining = ImplPrivateInlining(p, context)
-
-      // Inline implementation private functions
-      val implPrivateEncoder = inox.transformers.ProgramEncoder(p)(implPrivateInlining)
-
-      if (debugImplPrivateInlining.isEnabled) {
-        debugImplPrivateInlining.debugEncoder(implPrivateEncoder)
-      }
-
       // We do not need to encode empty trees as chooses when generating the VCs,
       // as we rely on having empty trees to filter out some VCs.
-      val assertionEncoder = inox.transformers.ProgramEncoder(implPrivateEncoder.targetProgram)(assertions)
+      val assertionEncoder = inox.transformers.ProgramEncoder(p)(assertions)
 
       if (debugAssertions.isEnabled) {
         debugAssertions.debugEncoder(assertionEncoder)
@@ -128,7 +112,7 @@ class VerificationRun(override val pipeline: StainlessPipeline)
         reporter.debug(s"Generating VCs for functions: ${functions map { _.uniqueName } mkString ", "}")
       }
 
-      val vcGenEncoder = implPrivateEncoder andThen assertionEncoder
+      val vcGenEncoder = assertionEncoder
 
       val vcs = if (context.options.findOptionOrDefault(optTypeChecker))
         context.timers.verification.get("type-checker").run {