search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
243 stars 34 forks source link

solver returns undecipherable output #481

Closed LeventErkok closed 5 years ago

LeventErkok commented 5 years ago

Received via email from Joshua Moerman.

import Data.SBV
import Data.SBV.Set
import Data.SBV.Tuple

problem = do
    let x = tuple (empty :: SSet Bool, empty :: SSet Bool)
    y <- exists_
    return $ x ./= y

We get:

*** Data.SBV.interpretSet: Unable to process solver output.
***
*** Kind    : {SBool}
*** Received: EApp [ECon "_",ECon "as-array",ECon "k!1"]
*** Reason  : Expected a set value, but couldn't decipher the solver output.
***
*** This is either a bug or something SBV currently does not support.
*** Please report this as a feature request!

Because z3 is producing weird output. Filed here: https://github.com/Z3Prover/z3/issues/2517