From 7cb5bddda95a87b6972b65e1f787311fbf5ad224 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Wed, 10 Dec 2014 07:51:29 +0100
Subject: [PATCH] Fix TransformerWithPC with matches
---
src/main/scala/leon/purescala/TransformerWithPC.scala | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/purescala/TransformerWithPC.scala b/src/main/scala/leon/purescala/TransformerWithPC.scala
index 41bf10a03..423353da3 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)
--
GitLab