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