J. J. W. | 29 Mar 06:22 2013
Picon

Haskell SBV Package with Z3

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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Levent Erkok | 29 Mar 07:12 2013
Picon

Re: Haskell SBV Package with Z3

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 <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
J. J. W. | 29 Mar 09:42 2013
Picon

Re: Haskell SBV Package with Z3

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 <at> 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 <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Levent Erkok | 29 Mar 14:49 2013
Picon

Re: Haskell SBV Package with Z3

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 <at> 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 <at> 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 <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Levent Erkok | 29 Mar 14:58 2013
Picon

Re: Haskell SBV Package with Z3

Sorry, there were a couple of typos in the last example. It should read: 

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

Note that this will return all 255 values that satisfy this property; i.e., everything except 0. (Here, we're using "sat/allSat" as opposed to "prove,"  and hence the inversion of equality in the property.)

-Levent.


On Fri, Mar 29, 2013 at 6:49 AM, Levent Erkok <erkokl <at> gmail.com> wrote:
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 <at> 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 <at> 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 <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe




_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
J. J. W. | 31 Mar 16:12 2013
Picon

Re: Haskell SBV Package with Z3

Dear L. Erkok,

First I would like to wish you happy easter and I would like to thank you for your help.

I have a couple of more questions. I am now playing with SBV package, however I am not sure if I understand the use of arrays, maybe you can give me some pointers. For example I want to prove the following (note: this example is only used to illustrate my question, I thought I've read somewhere in Haddock that this method only support functions with 7 parameters?)

prove $ \(a :: SWord8) b c -> a .> b &&& b .> c ==> a .> c
Q.E.D.

how should I express this using SymArray? 

Thanks in advance!

Yours sincerely,

Jun Jie


2013/3/29 Levent Erkok <erkokl <at> gmail.com>
Sorry, there were a couple of typos in the last example. It should read: 

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

Note that this will return all 255 values that satisfy this property; i.e., everything except 0. (Here, we're using "sat/allSat" as opposed to "prove,"  and hence the inversion of equality in the property.)

-Levent.


On Fri, Mar 29, 2013 at 6:49 AM, Levent Erkok <erkokl <at> gmail.com> wrote:
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 <at> 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 <at> 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 <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe





_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Levent Erkok | 1 Apr 04:55 2013
Picon

Re: Haskell SBV Package with Z3

Jun Jie: A SymArray is an abstraction of an array that can contain symbolic values, as well as being indexed by a symbolic value. I'm not sure how the example you picked relates. There's a sample program in the SBV distribution that shows how to use SymArray's, maybe looking at that might help: http://hackage.haskell.org/packages/archive/sbv/2.10/doc/html/Data-SBV-Examples-Uninterpreted-AUF.html

Feel free to e-mail me privately for further questions on SBV; the mailing list might not be quite appropriate for detailed discussions.

-Levent.


On Sun, Mar 31, 2013 at 7:12 AM, J. J. W. <bsc.j.j.w <at> gmail.com> wrote:
Dear L. Erkok,

First I would like to wish you happy easter and I would like to thank you for your help.

I have a couple of more questions. I am now playing with SBV package, however I am not sure if I understand the use of arrays, maybe you can give me some pointers. For example I want to prove the following (note: this example is only used to illustrate my question, I thought I've read somewhere in Haddock that this method only support functions with 7 parameters?)

prove $ \(a :: SWord8) b c -> a .> b &&& b .> c ==> a .> c
Q.E.D.

how should I express this using SymArray? 

Thanks in advance!

Yours sincerely,

Jun Jie


2013/3/29 Levent Erkok <erkokl <at> gmail.com>
Sorry, there were a couple of typos in the last example. It should read: 

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

Note that this will return all 255 values that satisfy this property; i.e., everything except 0. (Here, we're using "sat/allSat" as opposed to "prove,"  and hence the inversion of equality in the property.)

-Levent.


On Fri, Mar 29, 2013 at 6:49 AM, Levent Erkok <erkokl <at> gmail.com> wrote:
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 <at> 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 <at> 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 <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe






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

Gmane