Skip to content
Snippets Groups Projects
Commit 12154513 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

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.
parent 08336814
No related branches found
No related tags found
No related merge requests found
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment