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