[Haskell-cafe] Installing Z3 on OS X 10.8.4 ( Off topic )

[mukesh tiwari]

Hello all,
Not directly related to Haskell but I am trying to install Z3 to use SBV
package[1]. I followed the instructions[2]  to  install it.

*Mukeshs-MacBook-Pro:SMT mukeshtiwari$ git clone
https://git01.codeplex.com/z3 -b unstable
Cloning into 'z3'...
remote: Counting objects: 16070, done.
remote: Compressing objects: 100% (3928/3928), done.
remote: Total 16070 (delta 12057), reused 16070 (delta 12057)
Receiving objects: 100% (16070/16070), 7.62 MiB | 287 KiB/s, done.
Resolving deltas: 100% (12057/12057), done.*

After installing Z3
*Running python example.py in z3/examples/python gives this result.
*
*Mukeshs-MacBook-Pro:python mukeshtiwari$ python example.py
sat
[y = 4, x = 2]*

but when I am running sbv package, I am getting this error.

*Mukeshs-MacBook-Pro:site-packages mukeshtiwari$ ghci -XScopedTypeVariables
GHCi, version 7.6.1: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :m Data.SBV.Bridge.Z3
Prelude Data.SBV.Bridge.Z3> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x
Loading package pretty-1.1.1.0 ... linking ... done.
Loading package array-0.4.0.1 ... linking ... done.
Loading package deepseq-1.3.0.1 ... linking ... done.
Loading package filepath-1.3.0.1 ... linking ... done.
Loading package old-locale-1.0.0.5 ... linking ... done.
Loading package time-1.4.0.1 ... linking ... done.
Loading package bytestring-0.10.0.0 ... linking ... done.
Loading package unix-2.6.0.0 ... linking ... done.
Loading package directory-1.2.0.0 ... linking ... done.
Loading package process-1.1.0.2 ... linking ... done.
Loading package old-time-1.1.0.1 ... linking ... done.
Loading package containers-0.5.0.0 ... linking ... done.
Loading package random-1.0.1.1 ... linking ... done.
Loading package template-haskell ... linking ... done.
Loading package QuickCheck-2.5.1.1 ... linking ... done.
Loading package transformers-0.3.0.0 ... linking ... done.
Loading package mtl-2.1.2 ... linking ... done.
Loading package syb-0.3.7 ... linking ... done.
Loading package sbv-2.10 ... linking ... done.
*** An error occurred.
***  Unable to locate executable for z3
***  Executable specified: "z3"
Prelude Data.SBV.Bridge.Z3> *

I have posted every details on installation on pastebin[3]. The
documentation file says that[4] it will install

*2) Building Z3 using make/g++ and Python
Execute:

  autconf
  ./configure
  python scripts/mk_make.py
  cd build
  make
  sudo make install

It will install z3 executable at /usr/bin, libraries at /usr/lib, and
include files at /usr/include.*

Mukeshs-MacBook-Pro:z3 mukeshtiwari$ echo $PATH
/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin:/Users/mukeshtiwari/Programming/GHC/ghc-7.6.1/bin:/Users/mukeshtiwari/.cabal/bin:/Users/mukeshtiwari/Erlang/bin:/Users/mukeshtiwari/Programming/Scala/scala-2.10.0/bin:/usr/local/smlnj-110.75/bin:/Users/mukeshtiwari/.rvm/bin

Could some one please tell me how to solve this problem.

Regards,
Mukesh Tiwari


[1] http://hackage.haskell.org/package/sbv
[2]
http://z3.codeplex.com/wikipage?title=Building%20the%20unstable%20%28working-in-progress%29%20branch&referringTitle=Documentation
[3] http://pastebin.com/K5rq3jCF
[4] http://z3.codeplex.com/SourceControl/latest#README
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130701/df20d1a1/attachment.htm>