diff --git a/src/main/scala/leon/purescala/TransformerWithPC.scala b/src/main/scala/leon/purescala/TransformerWithPC.scala index a3655aaa13f0c3de61de487b7d53f2d934f116d7..9c6b4cad8ed3581432ca18d3629bac2e08dd7c21 100644 --- a/src/main/scala/leon/purescala/TransformerWithPC.scala +++ b/src/main/scala/leon/purescala/TransformerWithPC.scala @@ -26,10 +26,11 @@ abstract class TransformerWithPC extends Transformer { var soFar = path MatchExpr(rs, cases.map { c => - val patternExpr = conditionForPattern(rs, c.pattern, includeBinders = true) + val patternExprPos = conditionForPattern(rs, c.pattern, includeBinders = true) + val patternExprNeg = conditionForPattern(rs, c.pattern, includeBinders = false) - val subPath = register(patternExpr, soFar) - soFar = register(Not(patternExpr), soFar) + val subPath = register(patternExprPos, soFar) + soFar = register(Not(patternExprNeg), soFar) c match { case SimpleCase(p, rhs) =>