From 12154513488e8978060b674ab60f76c4fffd77ce Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Tue, 26 Aug 2014 10:37:30 +0200
Subject: [PATCH] Fix issues with phantom variables showing up in synthesis.
Previously if the choose was in the following context:
```
a match {
case Cons(h, t) =>
case _ =>
choose()
}
```
its path condition would include:
```
!(a.isInstanceOf[Cons] && a.head == h && a.tail == t)
```
which causes mostly unconstrained variables `h` and `t` to show up in the
synthesis problem.
---
src/main/scala/leon/purescala/TransformerWithPC.scala | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/purescala/TransformerWithPC.scala b/src/main/scala/leon/purescala/TransformerWithPC.scala
index a3655aaa1..9c6b4cad8 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) =>
--
GitLab