Exclude unsupported trees from ReturnElimination phase

jad-hamza · jad-hamza · commit 304b5a27069f · 2021-03-09T09:24:11.000+01:00
diff --git a/core/src/main/scala/stainless/extraction/imperative/ReturnElimination.scala b/core/src/main/scala/stainless/extraction/imperative/ReturnElimination.scala
@@ -415,6 +415,9 @@ trait ReturnElimination
           }
           processBlockExpressions(es :+ last)
 
+        case (_: s.Lambda | _: s.Forall | _: s.Old | _: s.Snapshot | _: s.Choose) =>
+          SimpleWhileTransformer.transform(expr)
+
         case _ if exprHasReturn(expr) =>
           val (ids, vs, es, tps, flags, recons) = deconstructor.deconstruct(expr)
           val tvs = vs.map(SimpleWhileTransformer.transform).map(_.asInstanceOf[t.Variable])

Original file line number	Diff line number	Diff line change
`@@ -415,6 +415,9 @@ trait ReturnElimination`
`415`	`415`	`}`
`416`	`416`	`processBlockExpressions(es :+ last)`
`417`	`417`
	`418`	`+ case (_: s.Lambda \| _: s.Forall \| _: s.Old \| _: s.Snapshot \| _: s.Choose) =>`
	`419`	`+ SimpleWhileTransformer.transform(expr)`
	`420`	`+`
`418`	`421`	`case _ if exprHasReturn(expr) =>`
`419`	`422`	`val (ids, vs, es, tps, flags, recons) = deconstructor.deconstruct(expr)`
`420`	`423`	`val tvs = vs.map(SimpleWhileTransformer.transform).map(_.asInstanceOf[t.Variable])`