[Haskell-cafe] Haskell SBV Package with Z3

[J. J. W.]

Dear all,

I have a small question regarding the installation of the SBV package. I
first installed the SBV 2.10 package with cabal with the following
instructions:

cabal install sbv

Next I installed the Z3 theorem prover and adding the path to my system
variables (Windows 7 x64). Next I tested whether I could find it by opening
cmd.exe and then typing z3, I get an error message of Z3, so I can safely
assume the system can find it. (I added the path to the bin of Z3, I have
not included the include directory, I see no reason why I should add a path
to this directory, but maybe I am wrong).

I ran the program: SBVUnitTests. However it had some errors in the
beginning and afterwards a few failures. Having no idea how to fix this, I
continued to check whether I can get the SBV to work. So I started to
execute the SBV package:

ghci -XScopedTypeVariables
ghci> :m Data.SBV
ghci> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x

Now this should return Q.E.D., however it returned the following:

An error occured.
Failed to complete the call to z3
Executable: "C:\\Program Files\\z3-4.3.0-x64\\bin\\z3.exe
Options: /in /smt2
Exit code: 0
Solver output:
===========================================================
; :smt.mbqi
; :pp.decimal_precision
===========================================================

Giving up..

It does seems like that the Z3 has a normal output, however not a result.
Can someone help me to figure out what I actually did wrong?

I am using Z3 version 4.3.0, SBV 2.10 and GHCi 7.4.2

Thank you for your help!

Yours sincerely,

Jun Jie
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130329/d712557d/attachment.htm>