Add unchecked annotation to inlined body

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

@@ -73,7 +73,7 @@ trait FunctionInlining extends CachingPhase with IdentitySorts { self =>
         val specced = BodyWithSpecs(tfd.fullBody)
         // simple path for inlining when all arguments are values, and the function's body doesn't contain other function invocations
         if (specced.specs.isEmpty && args.forall(isValue) && !exprOps.containsFunctionCalls(tfd.fullBody)) {
-          exprOps.replaceFromSymbols(tfd.params.zip(args).toMap, exprOps.freshenLocals(tfd.fullBody))
+          annotated(exprOps.replaceFromSymbols(tfd.params.zip(args).toMap, exprOps.freshenLocals(tfd.fullBody)), Unchecked)
         } else {
           // We need to keep the body as-is for `@synthetic` methods, such as
           // `copy` or implicit conversions for implicit classes, in order to
@@ -119,15 +119,10 @@ trait FunctionInlining extends CachingPhase with IdentitySorts { self =>
             case _ => e
           }
 
-
           val res = ValDef.fresh("inlined", tfd.returnType)
           val inlined = addPreconditionAssertions(addPostconditionAssumption(body))
 
-          // We bind the inlined expression in a let to avoid propagating
-          // the @unchecked annotation to postconditions, etc.
-          val newBody = let(res, inlined, res.toVariable.setPos(fi)).setPos(fi)
-
-          val result = (tfd.params zip args).foldRight(newBody) {
+          val result = (tfd.params zip args).foldRight(inlined) {
             case ((vd, e), body) => let(vd, e, body).setPos(fi)
           }
 

frontends/benchmarks/verification/invalid/InliningUnchecked.scala

@@ -0,0 +1,9 @@
+object InliningUnchecked {
+
+  @inline def f: Int = 0
+
+  def g: Int = {
+    f
+  }.ensuring(_ == 10)
+
+}