diff --git a/src/main/scala/leon/purescala/TransformerWithPC.scala b/src/main/scala/leon/purescala/TransformerWithPC.scala index 41bf10a03a50b3cc3b182918617901e29dcc027a..423353da38bbeb35ee2ef25d2fd1164957f464dd 100644 --- a/src/main/scala/leon/purescala/TransformerWithPC.scala +++ b/src/main/scala/leon/purescala/TransformerWithPC.scala @@ -32,9 +32,11 @@ abstract class TransformerWithPC extends Transformer { MatchExpr(rs, cases.map { c => val patternExprPos = conditionForPattern(rs, c.pattern, includeBinders = true) val patternExprNeg = conditionForPattern(rs, c.pattern, includeBinders = false) + val map = mapForPattern(rs, c.pattern) + val guard = replaceFromIDs(map, c.optGuard.getOrElse(BooleanLiteral(true))) val subPath = register(patternExprPos, soFar) - soFar = register(Not(patternExprNeg), soFar) + soFar = register(not(and(patternExprNeg, guard)), soFar) MatchCase(c.pattern, c.optGuard, rec(c.rhs,subPath)).copiedFrom(c)