diff --git a/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala b/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala
index 77d5ad5d5..e81f38a7b 100644
--- a/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala
+++ b/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
diff --git a/frontends/benchmarks/imperative/valid/FreshExpr.scala b/frontends/benchmarks/imperative/valid/FreshExpr1.scala
similarity index 99%
rename from frontends/benchmarks/imperative/valid/FreshExpr.scala
rename to frontends/benchmarks/imperative/valid/FreshExpr1.scala
index a7659d359..ae762831e 100644
--- a/frontends/benchmarks/imperative/valid/FreshExpr.scala
+++ b/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)
diff --git a/frontends/benchmarks/imperative/valid/FreshExpr2.scala b/frontends/benchmarks/imperative/valid/FreshExpr2.scala
new file mode 100644
index 000000000..795e4bdc1
--- /dev/null
+++ b/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
+    }
+  }
+}
\ No newline at end of file