From e22e91a7e22e40d8d1c3061f28308c4936531533 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Viktor=20Kun=C4=8Dak?= <vkuncak@users.noreply.github.com>
Date: Tue, 5 Nov 2024 11:17:05 +0100
Subject: [PATCH] Bumped compiler version to 3.5.2 and removed a patmat warning
 (#1599)

* Bumped compiler version to 3.5.2 and removed a patmat warning

* Depend on Inox module compiled with 3.5.2

* bump sbt plugin

---------

Co-authored-by: Samuel Chassot <samuel.chassot@epfl.ch>
---
 bin/package-sbt-plugin.sh                                     | 4 ++--
 build.sbt                                                     | 4 ++--
 .../stainless/extraction/inlining/FunctionInlining.scala      | 1 +
 inox                                                          | 2 +-
 sbt-plugin/src/sbt-test/sbt-plugin/ghost/test                 | 2 +-
 sbt-plugin/src/sbt-test/sbt-plugin/simple/test                | 2 +-
 6 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/bin/package-sbt-plugin.sh b/bin/package-sbt-plugin.sh
index 4e2c82fdc..e9e874dd7 100755
--- a/bin/package-sbt-plugin.sh
+++ b/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"
diff --git a/build.sbt b/build.sbt
index 2206aa929..74c37aed1 100644
--- a/build.sbt
+++ b/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
diff --git a/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala b/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala
index 097152f2c..affbfed32 100644
--- a/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala
+++ b/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
           }
 
diff --git a/inox b/inox
index 6062f8f95..7fdb9442f 160000
--- a/inox
+++ b/inox
@@ -1 +1 @@
-Subproject commit 6062f8f9552e5f71d441d7d0365bcb17e67fc224
+Subproject commit 7fdb9442ff33ffcf57c58e269387dac0991b78e1
diff --git a/sbt-plugin/src/sbt-test/sbt-plugin/ghost/test b/sbt-plugin/src/sbt-test/sbt-plugin/ghost/test
index 1e6202387..f466dd41d 100644
--- a/sbt-plugin/src/sbt-test/sbt-plugin/ghost/test
+++ b/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
diff --git a/sbt-plugin/src/sbt-test/sbt-plugin/simple/test b/sbt-plugin/src/sbt-test/sbt-plugin/simple/test
index 72e19611a..9540cd6d2 100644
--- a/sbt-plugin/src/sbt-test/sbt-plugin/simple/test
+++ b/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