Bumped compiler version to 3.5.2 and removed a patmat warning

bin/package-sbt-plugin.sh

@@ -6,8 +6,8 @@ if [[ $(git diff --stat) != '' ]]; then
   STAINLESS_VERSION="$STAINLESS_VERSION-SNAPSHOT"
 fi
 
-SCALA_VERSION="3.5.0"
-SCALA_LIB_VERSION="3.5.0"
+SCALA_VERSION="3.5.2"
+SCALA_LIB_VERSION="3.5.2"
 PUBLISHED_SBT_PLUGIN_DIR="$HOME/.ivy2/local/ch.epfl.lara/sbt-stainless/scala_2.12/sbt_1.0/$STAINLESS_VERSION"
 LIB_SCALA_VERSION_JAR_NAME_PART=$(echo $SCALA_LIB_VERSION | cut -d '.' -f 1)
 PUBLISHED_LIB_DIR="$HOME/.ivy2/local/ch.epfl.lara/stainless-library_$LIB_SCALA_VERSION_JAR_NAME_PART/$STAINLESS_VERSION"

build.sbt

@@ -40,9 +40,9 @@ lazy val nTestSuiteParallelism = {
 
 // The Scala version with which Stainless is compiled.
 // Note: in case of version bump, do not forget to update the `test` files in `sbt-plugin` (for `sbt scripted`)!
-val stainlessScalaVersion = "3.5.0"
+val stainlessScalaVersion = "3.5.2"
 val frontendDottyVersion = stainlessScalaVersion
-// The Stainless libraries use Scala 2.13 and Scala 3.3, and is compatible only with Scala 3.3.
+// The Stainless libraries use Scala 2.13 and Scala 3.5, and is compatible only with Scala 3.5.
 val stainlessLibScalaVersion = stainlessScalaVersion
 
 scalaVersion := stainlessScalaVersion

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

@@ -88,6 +88,7 @@ class FunctionInlining(override val s: Trees, override val t: trace.Trees)
                   Assert(annotated(cond.setPos(fi), DropVCs), Some(s"Inlined precondition$num of " + tfd.id.asString), acc).setPos(fi),
                   i-1
                 )
+              case (spec, (acc,i)) => context.reporter.fatalError(f"In addPreconditionAssertions, I did not expect spec that is not LetInSpec or Precondition; I got the following spec: ${spec.toString}")
             }._1
           }
 

sbt-plugin/src/sbt-test/sbt-plugin/ghost/test

@@ -1,5 +1,5 @@
 > + tailrec/run
 > + basic/run
-$ exists basic/target/scala-3.5.0/classes/test/Main.class
+$ exists basic/target/scala-3.5.2/classes/test/Main.class
 $ absent basic/target/sneakyGhostCalled basic/target/insideGhostCalled
 > + actor-tests/compile

sbt-plugin/src/sbt-test/sbt-plugin/simple/test

@@ -1,5 +1,5 @@
 > assertLogMessage
 > + success/compile
 # check that a module on which stainless verification passes compiles fine (i.e., binaries are produced)
-$ exists success/target/scala-3.5.0/classes/Extern1.class
+$ exists success/target/scala-3.5.2/classes/Extern1.class
 # > failure/checkScalaFailures