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