Avoid duplication of scrutinee in lowered matches (from #860)

epfl-lara · Jan 16, 2021 · 37eafa4 · 37eafa4
1 parent 5cfd22f
commit 37eafa4
Showing 1 changed file with 5 additions and 3 deletions.
diff --git a/core/src/main/scala/stainless/ast/SymbolOps.scala b/core/src/main/scala/stainless/ast/SymbolOps.scala
@@ -144,9 +144,11 @@ trait SymbolOps extends inox.ast.SymbolOps { self: TypeOps =>
 
     def rewritePM(e: Expr): Option[Expr] = e match {
       case m @ MatchExpr(scrut, cases) =>
+        val scrutVd = ValDef.fresh("scrut", scrut.getType).setPos(m)
+        val scrutV = scrutVd.toVariable
         val condsAndRhs = for (cse <- cases) yield {
-          val map = mapForPattern(scrut, cse.pattern)
-          val patCond = conditionForPattern[Path](scrut, cse.pattern, includeBinders = false)
+          val map = mapForPattern(scrutV, cse.pattern)
+          val patCond = conditionForPattern[Path](scrutV, cse.pattern, includeBinders = false)
           val realCond = cse.optGuard match {
             case Some(g) => patCond withCond replaceFromSymbols(map, g)
             case None => patCond
@@ -170,7 +172,7 @@ trait SymbolOps extends inox.ast.SymbolOps { self: TypeOps =>
           }
         })
 
-        Some(bigIte)
+        Some(Let(scrutVd, scrut, bigIte).copiedFrom(m))
 
       case _ => None
     }