Skip to content
Snippets Groups Projects
user avatar
Etienne Kneuss authored
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.
12154513
History
Name Last commit Last update