From bc2eb7249d2d97d588ba91480bf20b6afc882305 Mon Sep 17 00:00:00 2001 From: Georg Stefan Schmid Date: Sat, 16 Jan 2021 16:24:26 +0100 Subject: [PATCH] Avoid duplication of scrutinee in lowered matches (from #860) --- core/src/main/scala/stainless/ast/SymbolOps.scala | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/core/src/main/scala/stainless/ast/SymbolOps.scala b/core/src/main/scala/stainless/ast/SymbolOps.scala index 5280ab77d3..590410df66 100644 --- 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 }