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