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

Tables in smtFunction #666

Closed LeventErkok closed 9 months ago

LeventErkok commented 1 year ago 
import Data.SBV

foo :: SInteger -> SWord32
foo = smtFunction "foo" (\x -> select [1,2,3] 0 x)

We get:

Main> satWith z3{verbose=True} $ \x -> foo x .== 2

chokes terribly:

*** Exception:
*** Data.SBV: Unexpected non-success response from Z3:
***
***    Sent      : (assert (= (table0 0) l1_s1))
***    Expected  : success
***    Received  : (error "line 21 column 22: unknown constant l1_s1")
***
***    Exit code : ExitFailure (-15)
***    Executable: /usr/local/bin/z3
***    Options   : -nw -in -smt2