Address warnings

build.sbt

@@ -275,7 +275,7 @@ val scriptSettings: Seq[Setting[_]] = Seq(
 def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
 
 // lazy val inox = RootProject(file("../inox"))
-lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "8b360ea16e7049f5ecfb140f001971745cf9f9ad")
+lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "1c8c0bac611ad4edc2c5b209deea9c75359d51b1")
 lazy val cafebabe = ghProject("https://github.com/epfl-lara/cafebabe.git", "616e639b34379e12b8ac202849de3ebbbd0848bc")
 
 // Allow integration test to use facilities from regular tests

core/src/main/scala/stainless/extraction/imperative/ReturnElimination.scala

@@ -270,11 +270,14 @@ class ReturnElimination(override val s: Trees, override val t: Trees)
                 // postcondition of the top-level function hold
                 v => t.SplitAnd.many(
                   optInvChecked.getOrElse(t.BooleanLiteral(true).copiedFrom(wh)),
-                  topLevelPost.map { case s.exprOps.Postcondition(s.Lambda(Seq(postVd), postBody)) =>
-                    t.exprOps.replaceFromSymbols(
-                      Map(simpleWhileTransformer.transform(postVd) -> v),
-                      simpleWhileTransformer.transform(postBody)
-                    )(using t.convertToVal)
+                  topLevelPost.map {
+                    case s.exprOps.Postcondition(s.Lambda(Seq(postVd), postBody)) =>
+                      t.exprOps.replaceFromSymbols(
+                        Map(simpleWhileTransformer.transform(postVd) -> v),
+                        simpleWhileTransformer.transform(postBody)
+                      )(using t.convertToVal)
+                    case s.exprOps.Postcondition(l @ s.Lambda(_, _)) =>
+                      sys.error(s"Unexpected number of params for postcondition lambda: $l")
                   }.getOrElse(t.BooleanLiteral(true)),
                 ),
                 // when the while loop terminates without returning, we check the loop condition

core/src/main/scala/stainless/extraction/inlining/ChooseInjector.scala

@@ -69,8 +69,11 @@ class ChooseInjector(override val s: inlining.Trees,
 
     if (context.toReplace.contains(fd.id)) {
       val choose = post
-        .map { case Postcondition(Lambda(Seq(vd), post)) =>
-          Choose(vd, freshenLocals(specced.wrapLets(post)))
+        .map {
+          case Postcondition(Lambda(Seq(vd), post)) =>
+            Choose(vd, freshenLocals(specced.wrapLets(post)))
+          case Postcondition(l @ Lambda(_, _)) =>
+            sys.error(s"Unexpected number of params for postcondition lambda: $l")
         }
         .getOrElse {
           Choose(ValDef(FreshIdentifier("res", true), fd.returnType), BooleanLiteral(true))

core/src/main/scala/stainless/extraction/inlining/FunctionSpecialization.scala

@@ -225,6 +225,8 @@ class FunctionSpecialization(override val s: Trees)(override val t: s.type)
             val cond = and(cond1, exprOps.replaceFromSymbols(Map(res2 -> res1.toVariable), cond2))
             Postcondition(Lambda(Seq(res1), cond.copiedFrom(cond2)).copiedFrom(lam2))
               .setPos(pc2.getPos)
+          case (Postcondition(l1 @ Lambda(_, _)), Postcondition(l2 @ Lambda(_, _))) =>
+            sys.error(s"Unexpected number of params for postcondition lambdas: $l1 and $l2")
         },
         mergeOptions(specced1.getSpec(PreconditionKind), speccedOuter.getSpec(PreconditionKind)) {
           case (Precondition(cond1), pc2 @ Precondition(cond2)) =>

core/src/main/scala/stainless/extraction/innerclasses/InnerClasses.scala

@@ -121,7 +121,6 @@ class InnerClasses(override val s: Trees, override val t: methods.Trees)
         outerRefs map {
           case ValDef(_, ct: ClassType, _) if currentClass.id == ct.id => thiss
           case ValDef(id, _, _) => ClassSelector(thiss, id)
-          case _ => sys.error("Unreachable") // To silence false positive warning
         }
       }
     }

core/src/main/scala/stainless/extraction/oo/RefinementLifting.scala

@@ -218,6 +218,8 @@ class RefinementLifting(override val s: Trees, override val t: Trees)
           Some(s.Lambda(Seq(res), s.and(
               exprOps.replaceFromSymbols(Map(vd2 -> res.toVariable), pred),
               body).copiedFrom(body)).copiedFrom(post))
+        case Some(post @ s.Lambda(_, _)) =>
+          sys.error(s"Unexpected number of params for postcondition lambda: $post")
         case None =>
           Some(s.Lambda(Seq(vd2), pred).copiedFrom(fd))
       }

core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala

@@ -655,10 +655,10 @@ class TypeEncoding(override val s: Trees, override val t: Trees)
       val tout = out.map(tp => scope.transform(tp).asInstanceOf[t.TypeParameter])
 
       val x = "x" :: T(id)(tin: _*)
-      val fs = tin zip tout flatMap { case (i, o) => Seq(i.id.name :: (i =>: o), i.id.name :: (o =>: i)) }
+      val fs = tin zip tout map { case (i, o) => (i.id.name :: (i =>: o), i.id.name :: (o =>: i)) }
 
-      val newScope = scope converting (in zip out zip fs.grouped(2).toSeq flatMap {
-        case ((ti, to), Seq(vd1, vd2)) => Seq((ti, to) -> vd1.toVariable, (to, ti) -> vd2.toVariable)
+      val newScope = scope converting (in zip out zip fs flatMap {
+        case ((ti, to), (vd1, vd2)) => Seq((ti, to) -> vd1.toVariable, (to, ti) -> vd2.toVariable)
       })
 
       val conversions = sort.typed(in).constructors zip sort.typed(out).constructors map { case (ci, co) =>
@@ -672,7 +672,7 @@ class TypeEncoding(override val s: Trees, override val t: Trees)
       }
 
       new t.FunDef(
-        convertID(id), (tin ++ tout).map(t.TypeParameterDef(_)), x +: fs, T(id)(tout: _*), fullBody,
+        convertID(id), (tin ++ tout).map(t.TypeParameterDef(_)), x +: fs.flatMap((vd1, vd2) => Seq(vd1, vd2)), T(id)(tout: _*), fullBody,
         Seq(t.DropVCs, t.Synthetic)
       ).setPos(sort)
     }
@@ -1240,6 +1240,8 @@ class TypeEncoding(override val s: Trees, override val t: Trees)
       val specced = t.exprOps.BodyWithSpecs(encoded.fullBody)
       val (vd, post) = specced.getSpec(t.exprOps.PostconditionKind) match {
         case Some(t.exprOps.Postcondition(Lambda(Seq(vd), post))) => (vd, post)
+        case Some(t.exprOps.Postcondition(l @ Lambda(_, _))) =>
+          sys.error(s"Unexpected number of params for postcondition lambda: $l")
         case None => (
           t.ValDef.fresh("res", encoded.returnType),
           t.BooleanLiteral(true).copiedFrom(encoded.fullBody)

core/src/main/scala/stainless/extraction/trace/Trace.scala

@@ -50,7 +50,7 @@ class Trace(override val s: Trees, override val t: termination.Trees)
         val returnType = s.UnitType()
 
         val specsMap = (fd1.params zip newParamVars).toMap
-        val specs = BodyWithSpecs(fd1.fullBody).specs.filter(s => s.kind == LetKind || s.kind == PreconditionKind) 
+        val specs = BodyWithSpecs(fd1.fullBody).specs.filter(s => s.kind == LetKind || s.kind == PreconditionKind)
         val pre = specs.map(spec => spec match {
           case Precondition(cond) => Precondition(exprOps.replaceFromSymbols(specsMap, cond))
           case LetInSpec(vd, expr) => LetInSpec(vd, exprOps.replaceFromSymbols(specsMap, expr))
@@ -96,7 +96,7 @@ class Trace(override val s: Trees, override val t: termination.Trees)
       fd.flags.filter(elem => elem.name == "traceInduct").head match {
         case s.Annotation("traceInduct", fun) => {
           BodyWithSpecs(fd.fullBody).getSpec(PostconditionKind) match {
-            case Some(Postcondition(post)) => 
+            case Some(Postcondition(post)) =>
               s.exprOps.preTraversal {
                 case _ if funInv.isDefined => // do nothing
                 case fi @ s.FunctionInvocation(tfd, _, args) if symbols.isRecursive(tfd) && (fun.contains(StringLiteral(tfd.name)) || fun.contains(StringLiteral("")))
@@ -105,9 +105,9 @@ class Trace(override val s: Trees, override val t: termination.Trees)
                       val argCheck = args.forall(paramVars.contains) && args.toSet.size == args.size
                       if (argCheck) funInv = Some(fi)
                     }
-                case _ => 
+                case _ =>
               }(post)
-            case _ => 
+            case _ =>
           }
         }
       }
@@ -141,7 +141,7 @@ class Trace(override val s: Trees, override val t: termination.Trees)
     } else List())
 
     val extractedSymbols = super.extractSymbols(context, symbols)
-    
+
     val extracted = t.NoSymbols
       .withSorts(extractedSymbols.sorts.values.toSeq)
       .withFunctions(extractedSymbols.functions.values.filterNot(fd => fd.flags.exists(elem => elem.name == "traceInduct")).toSeq)
@@ -188,7 +188,7 @@ class Trace(override val s: Trees, override val t: termination.Trees)
 
     val subst = (model.params.map(_.id) zip fi.args).toMap
     val specializer = new Specializer(model, indPattern.id, subst)
-    
+
     val fullBodySpecialized = specializer.transform(exprOps.withoutSpecs(model.fullBody).get)
 
     val specsMap = (lemma.params zip newParamVars).toMap ++ (model.params zip newParamVars).toMap
@@ -203,13 +203,13 @@ class Trace(override val s: Trees, override val t: termination.Trees)
 
     val withPre = exprOps.reconstructSpecs(pre, Some(fullBodySpecialized), indPattern.returnType)
 
-    val speccedLemma = BodyWithSpecs(lemma.fullBody).addPost
-    val speccedOrig = BodyWithSpecs(model.fullBody).addPost
-    val postLemma = speccedLemma.getSpec(PostconditionKind).map(post => exprOps.replaceFromSymbols(specsMap, post.expr))
-    val postOrig = speccedOrig.getSpec(PostconditionKind).map(post => exprOps.replaceFromSymbols(specsMap, post.expr))
-    
+    val speccedLemma = BodyWithSpecs(lemma.fullBody).addPost.getSpec(PostconditionKind).getOrElse(sys.error("Infallible (due to being specced)"))
+    val speccedOrig = BodyWithSpecs(model.fullBody).addPost.getSpec(PostconditionKind).getOrElse(sys.error("Infallible (due to being specced)"))
+    val postLemma = exprOps.replaceFromSymbols(specsMap, speccedLemma.expr)
+    val postOrig = exprOps.replaceFromSymbols(specsMap, speccedOrig.expr)
+
     (postLemma, postOrig) match {
-      case (Some(Lambda(Seq(res1), cond1)), Some(Lambda(Seq(res2), cond2))) => 
+      case (Lambda(Seq(res1), cond1), Lambda(Seq(res2), cond2)) =>
         val res = ValDef.fresh("res", indPattern.returnType)
         val freshCond1 = exprOps.replaceFromSymbols(Map(res1 -> res.toVariable), cond1)
         val freshCond2 = exprOps.replaceFromSymbols(Map(res2 -> res.toVariable), cond2)
@@ -219,6 +219,8 @@ class Trace(override val s: Trees, override val t: termination.Trees)
         indPattern.copy(
           fullBody = BodyWithSpecs(withPre).withSpec(post).reconstructed
         ).copiedFrom(indPattern)
+      case (l1 @ Lambda(_, _), l2 @ Lambda(_, _)) =>
+        sys.error(s"Unexpected number of params for postcondition lambdas: $l1 and $l2")
     }
 
   }
@@ -258,13 +260,13 @@ object Trace {
   var wrong: List[Identifier] = List() //bad signature
 
   def optionsError(using ctx: inox.Context): Boolean =
-    !ctx.options.findOptionOrDefault(frontend.optBatchedProgram) && 
+    !ctx.options.findOptionOrDefault(frontend.optBatchedProgram) &&
     (!ctx.options.findOptionOrDefault(optModels).isEmpty || !ctx.options.findOptionOrDefault(optCompareFuns).isEmpty)
-        
+
   def printEverything(using ctx: inox.Context) = {
     import ctx.{ reporter, timers }
     if (!clusters.isEmpty || !errors.isEmpty || !unknowns.isEmpty || !wrong.isEmpty) {
-      reporter.info(s"Printing equivalence checking results:")  
+      reporter.info(s"Printing equivalence checking results:")
       allModels.foreach(model => {
         val l = clusters(model).map(CheckFilter.fixedFullName).mkString(", ")
         val m = CheckFilter.fixedFullName(model)
@@ -331,10 +333,9 @@ object Trace {
 
   //iterate model for the current function
   def nextModel = tmpModels match {
-    case x::xs => { 
+    case x::xs =>
       tmpModels = xs
       model = Some(x)
-    }
     case Nil => model = None
   }
 

core/src/main/scala/stainless/termination/ChainProcessor.scala

@@ -72,8 +72,7 @@ class ChainProcessor(override val checker: ProcessingPipeline)
                 s"No measure annotated in function `${fd.id}` which was cleared in chain processor.")
           }
         })
-      case (Seq(), _, _) =>
-        None
+      case _ => None
     }
   }
 

core/src/main/scala/stainless/termination/MeasureInference.scala

@@ -214,6 +214,8 @@ class MeasureInference(override val s: Trees, override val t: Trees)(using overr
           val newNBody: t.Expr = t.exprOps.replaceFromSymbols(newMap, nbody)(using t.convertToVal)
           val refinement = t.RefinementType(newVd, newNBody)
           original.copy(returnType = refinement).copiedFrom(original)
+        case Some(post@t.Lambda(_, _)) =>
+          sys.error(s"Unexpected number of params for postcondition lambda: $post")
         case None       => original
       }
     }

core/src/main/scala/stainless/transformers/PartialEvaluator.scala

@@ -62,6 +62,8 @@ trait PartialEvaluator extends SimplifierWithPC { self =>
               Let(res, body, Assert(post,
                 Some("Inlined postcondition of " + tfd.id.name), res.toVariable).copiedFrom(lambda)
               ).copiedFrom(body)
+            case Postcondition(lambda @ Lambda(_, _)) =>
+              sys.error(s"Unexpected number of params for postcondition lambda: $lambda")
           } .getOrElse(body)
 
           val bodyPrePost = exprOps.preconditionOf(tfd.fullBody).map { case pre =>

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

@@ -47,8 +47,11 @@ class ChooseInjector private(val trees: ast.Trees)
 
         val newSpecced = if ((fd.flags contains Extern) || (fd.flags contains Opaque)) {
           val choose = post
-            .map { case Postcondition(Lambda(Seq(vd), post)) =>
-              Choose(vd, freshenLocals(specced.wrapLets(post)))
+            .map {
+              case Postcondition(Lambda(Seq(vd), post)) =>
+                Choose(vd, freshenLocals(specced.wrapLets(post)))
+              case Postcondition(l @ Lambda(_, _)) =>
+                sys.error(s"Unexpected number of params for postcondition lambda: $l")
             }
             .getOrElse {
               Choose(ValDef(FreshIdentifier("res", true), fd.returnType), BooleanLiteral(true))

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

@@ -454,6 +454,8 @@ trait CoqEncoder {
         case None => transformType(fd.returnType)
         case Some(Lambda(Seq(vd), post)) =>
           Refinement(makeFresh(vd.id), transformType(vd.tpe), transformTree(post) === trueBoolean)
+        case Some(l @ Lambda(_, _)) =>
+          sys.error(s"Unexpected number of params for postcondition lambda: $l")
       }
       val allParams = tparams ++ params ++ preconditionParam
       val tmp = if (fd.isRecursive) {

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

@@ -281,6 +281,8 @@ trait VerificationChecker { self =>
 
           case Unsat if vc.satisfiability =>
             VCResult(VCStatus.Invalid(VCStatus.Unsatisfiable), s.getResultSolver.map(_.name), Some(time))
+
+          case _ => sys.error(s"Unreachable: $res")
         }
 
         case Failure(u: inox.Unsupported) =>

frontends/scalac/src/main/scala/stainless/frontends/scalac/ScalaCompiler.scala

@@ -98,8 +98,8 @@ class ScalaCompiler(settings: NSCSettings, val ctx: inox.Context, val callback:
      with Positions { self =>
 
   // Normally, we would initialize the fields with early-initializer. Since this feature has been dropped in Scala 3,
-  // we work-around that by definining a dummy class overriding all members.
-  // This ensure that these fields are correctly initialized
+  // we work-around that by defining a dummy class overriding all members.
+  // This ensure that these fields are correctly initialized.
   class StainlessExtractionImpl(override val global: self.type,
                                 override val phaseName: String,
                                 override val runsAfter: List[String],