You're welcome Jun Jie. 

Regarding getting a different counter example: That's perfectly normal. When SMT solvers build models they use random seeds. Furthermore, different versions of the same solver can use different algorithms/heuristics to arrive at the falsifying model. So, it's entirely expected that you get a different counter-example. You can turn the question around, and ask the solver to give you all counter-examples like this:

         allSat $ \x -> \(x::SWord8) -> x `shiftL` 2 .!= x

-Levent. 

On Mar 29, 2013, at 1:42 AM, "J. J. W." <bsc.j.j.w@gmail.com> wrote:

Dear Levent,

Thank you for your support. I am very honoured to have the developer of the SBV package to solve my elementary problem. I noticed that the counter-example given by my Z3 differs from the one said on HackageDB: sbv-2.10.

Code that is on Hackage:

 Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x

   Falsifiable. Counter-example:

     x = 128 :: SWord8

My current GHCi output:

Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x

Falsifiable. Counter-example:

  x = 51 :: SWord8

(0.02 secs, 1196468 bytes)

Thank you for your help!

Yours sincerely,

Jun Jie

2013/3/29 Levent Erkok <erkokl@gmail.com>

Hi Jun Jie:

SBV uses some of the not-yet-officially-released features in Z3. The version you have, while it's the latest official Z3 release, will not work.

To resolve, you need to install the "development" version of Z3 (something that is at least 4.3.2 or better). Here're instructions from the Microsoft folks explaining how to get these builds: http://research.microsoft.com/en-us/um/people/leonardo/blog/2013/02/15/precompiled.html

Let me know if you find any issues after you get the latest-development version of Z3 installed.

-Levent.  

On Thu, Mar 28, 2013 at 10:22 PM, J. J. W. <bsc.j.j.w@gmail.com> wrote:

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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe