Merge branch 'main' into sam_reporting

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

@@ -701,7 +701,7 @@ trait EffectsAnalyzer extends oo.CachingPhase {
         val specced = BodyWithSpecs(symbols.simplifyLets(fi.inlined))
         specced.bodyOpt
           .map(specced.wrapLets)
-          .forall(isExpressionFresh)
+          .forall(rec(_, bindings))
 
       // other function invocations always return a fresh expression, by hypothesis (global assumption)
       case (_: FunctionInvocation | _: ApplyLetRec | _: Application) => true

frontends/benchmarks/imperative/valid/FreshExpr.scala → frontends/benchmarks/imperative/valid/FreshExpr1.scala

@@ -1,6 +1,6 @@
 import stainless.lang._
 
-object FreshExpr {
+object FreshExpr1 {
   case class C1(var c2: C2)
   case class C2(var c3: C3)
   case class C3(var bi: BigInt)

frontends/benchmarks/imperative/valid/FreshExpr2.scala

@@ -0,0 +1,18 @@
+import stainless.lang._
+
+object FreshExpr2 {
+
+  def iden(arr: Array[Int]) = arr
+
+  // Recursive functions must return fresh expression
+  def counting(i: Int): Array[Int] = {
+    require(0 <= i && i <= 10)
+    decreases(10 - i)
+    if (i < 10) {
+      counting(i + 1)
+    } else {
+      val b = Array.fill(0)(0)
+      iden(b) // This is a fresh expression
+    }
+  }
+}