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
239 stars 33 forks source link

allSat/skolemize incompatibility #672

Closed LeventErkok closed 9 months ago

LeventErkok commented 11 months ago 
Prelude Data.SBV> :set -XDataKinds
Prelude Data.SBV> sat $ skolemize $ \(Exists @"b" b) (Forall @"a" a) -> a .>= (b :: SWord8)
Satisfiable. Model:
  b = 0 :: Word8

But:

Prelude Data.SBV> allSat $ skolemize $ \(Exists @"b" b) (Forall @"a" a) -> a .>= (b :: SWord8)
*** Exception:
*** Data.SBV: Unexpected response from the solver, context: getModel:
***
***    Sent      : (get-value (s1))
***    Expected  : a value binding for kind: SWord8
***    Received  : (error "line 15 column 12: unknown constant s1")
***
***    Executable: z3
***    Options   : -nw -in -smt2
***
***    Reason    : Solver returned an error: "line 15 column 12: unknown constant s1"