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
244 stars 34 forks source link

Add support for boolector #60

Closed LeventErkok closed 11 years ago

LeventErkok commented 11 years ago

Investigate if we can integrate Boolector as a backend solver: http://fmv.jku.at/boolector/

LeventErkok commented 11 years ago

It appears boolector still doesn't support SMT-Lib2. While we can hook-up through the the SMT-Lib1 interface, it just is annoying to do so.. There's some talk that boolector might eventually support SMT-Lib2; especially come the next competition; so maybe it's worth waiting till then.