Skip to content
Snippets Groups Projects
  • Etienne Kneuss's avatar
    12154513
    Fix issues with phantom variables showing up in synthesis. · 12154513
    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
    Fix issues with phantom variables showing up in synthesis.
    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.