From 1705478da3820baf89dd2c3b8fb86d9d433f4658 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 30 Oct 2012 16:27:17 +0100
Subject: [PATCH] Always produce binders, and populate them with loads of women
---
src/main/scala/leon/purescala/TreeOps.scala | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index d00857b9c..e6b09cc17 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1153,7 +1153,9 @@ object TreeOps {
if (conditions contains fieldSel) {
computePatternFor(conditions(fieldSel), fieldSel)
} else {
- WildcardPattern(None)
+ val b = FreshIdentifier(id.name, true).setType(id.getType)
+ substMap += fieldSel -> Variable(b)
+ WildcardPattern(Some(b))
}
}
--
GitLab