mukesh tiwari | 1 Jul 11:27 2013
Picon

Installing Z3 on OS X 10.8.4 ( Off topic )

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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
mukesh tiwari | 1 Jul 12:12 2013
Picon

Re: Installing Z3 on OS X 10.8.4 ( Off topic )

I also tried installing Yices[1]  but still getting same error. I followed the instructions but still the same error. Seems like I am missing some crucial details about path but not able to resolve it.

Mukeshs-MacBook-Pro:SMT mukeshtiwari$ cd yices-2.1.0/
Mukeshs-MacBook-Pro:yices-2.1.0 mukeshtiwari$ ls
LICENSE        NOTICES        README        bin        doc        etc        examples    include        lib
Mukeshs-MacBook-Pro:yices-2.1.0 mukeshtiwari$ ls
LICENSE        NOTICES        README        bin        doc        etc        examples    include        lib
Mukeshs-MacBook-Pro:yices-2.1.0 mukeshtiwari$ cat README
Yices SMT Solver, Copyright SRI International, 2012
===================================================

This file is part of the Yices 2.0 binary distribution for MacOS X.
Yices is distributed free-of-charge for personal use under the terms
of the Yices license (see LICENSE).


Content
-------

This distribution includes three solvers

  bin/yices       (for the Yices 2 language)
  bin/yices-smt   (for SMT-LIB 1.2)
  bin/yices-sat   (sat solver, DIMACS format)

and the Yices libraries and header files

  lib/libyices.2.0.0.dylib
  include/yices.h
  include/yices_types.h
  include/yices_limits.h
  include/yices_exit_codes.h


Examples and documentation are in the examples and doc directories.


The binaries and library were linked statically against GMP version 5.0.4,
copyright Free Software Foundation (see NOTICES).



Recommended Library Installation on MacOS X
-------------------------------------------

The library's install name is '/usr/local/lib/libyices.2.dylib' so
the following procedure should be used to install it.

1) copy libyices.2.0.0.dylib in /usr/local/lib (this requires
   administrative privileges):

    sudo  cp libyices.2.0.0.dylib /usr/local/lib
    sudo  chmod 755 /usr/local/lib/libyices.2.0.0.dylib


2) add two symbolic links:

    sudo  ln -sf libyices.2.0.0.dylib /usr/local/lib/libyices.dylib
    sudo  ln -sf libyices.2.0.0.dylib /usr/local/lib/libyices.2.dylib




For more information, please visit http://yices.csl.sri.com.
Mukeshs-MacBook-Pro:yices-2.1.0 mukeshtiwari$ cd lib/
Mukeshs-MacBook-Pro:lib mukeshtiwari$ ls
libyices.2.1.0.dylib
Mukeshs-MacBook-Pro:lib mukeshtiwari$ sudo  cp libyices.2.1.0.dylib  /usr/local/lib
Password:
Mukeshs-MacBook-Pro:lib mukeshtiwari$ sudo  chmod 755 /usr/local/lib/libyices.2.1.0.dylib
Mukeshs-MacBook-Pro:lib mukeshtiwari$ sudo  ln -sf libyices.2.1.0.dylib /usr/local/lib/libyices.dylib
Mukeshs-MacBook-Pro:lib mukeshtiwari$ sudo  ln -sf libyices.2.1.0.dylib /usr/local/lib/libyices.2.dylib

Mukeshs-MacBook-Pro:~ 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.Yices
Prelude Data.SBV.Bridge.Yices> 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 Yices
***  Executable specified: "yices-smt"


Regards,
Mukesh Tiwari

[1] http://yices.csl.sri.com/download-yices2.shtml


On Mon, Jul 1, 2013 at 2:57 PM, mukesh tiwari <mukeshtiwari.iiitm <at> gmail.com> wrote:
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


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
mukesh tiwari | 1 Jul 12:47 2013
Picon

Re: Installing Z3 on OS X 10.8.4 ( Off topic )

Finally I got the Yices working by adding yices-2.1.0/bin to my path. Still looking to resolve Z3.

Regards,
Mukesh Tiwari


On Mon, Jul 1, 2013 at 3:42 PM, mukesh tiwari <mukeshtiwari.iiitm <at> gmail.com> wrote:
I also tried installing Yices[1]  but still getting same error. I followed the instructions but still the same error. Seems like I am missing some crucial details about path but not able to resolve it.

Mukeshs-MacBook-Pro:SMT mukeshtiwari$ cd yices-2.1.0/
Mukeshs-MacBook-Pro:yices-2.1.0 mukeshtiwari$ ls
LICENSE        NOTICES        README        bin        doc        etc        examples    include        lib
Mukeshs-MacBook-Pro:yices-2.1.0 mukeshtiwari$ ls
LICENSE        NOTICES        README        bin        doc        etc        examples    include        lib
Mukeshs-MacBook-Pro:yices-2.1.0 mukeshtiwari$ cat README
Yices SMT Solver, Copyright SRI International, 2012
===================================================

This file is part of the Yices 2.0 binary distribution for MacOS X.
Yices is distributed free-of-charge for personal use under the terms
of the Yices license (see LICENSE).


Content
-------

This distribution includes three solvers

  bin/yices       (for the Yices 2 language)
  bin/yices-smt   (for SMT-LIB 1.2)
  bin/yices-sat   (sat solver, DIMACS format)

and the Yices libraries and header files

  lib/libyices.2.0.0.dylib
  include/yices.h
  include/yices_types.h
  include/yices_limits.h
  include/yices_exit_codes.h


Examples and documentation are in the examples and doc directories.


The binaries and library were linked statically against GMP version 5.0.4,
copyright Free Software Foundation (see NOTICES).



Recommended Library Installation on MacOS X
-------------------------------------------

The library's install name is '/usr/local/lib/libyices.2.dylib' so
the following procedure should be used to install it.

1) copy libyices.2.0.0.dylib in /usr/local/lib (this requires
   administrative privileges):

    sudo  cp libyices.2.0.0.dylib /usr/local/lib
    sudo  chmod 755 /usr/local/lib/libyices.2.0.0.dylib


2) add two symbolic links:

    sudo  ln -sf libyices.2.0.0.dylib /usr/local/lib/libyices.dylib
    sudo  ln -sf libyices.2.0.0.dylib /usr/local/lib/libyices.2.dylib




For more information, please visit http://yices.csl.sri.com.
Mukeshs-MacBook-Pro:yices-2.1.0 mukeshtiwari$ cd lib/
Mukeshs-MacBook-Pro:lib mukeshtiwari$ ls
libyices.2.1.0.dylib
Mukeshs-MacBook-Pro:lib mukeshtiwari$ sudo  cp libyices.2.1.0.dylib  /usr/local/lib
Password:
Mukeshs-MacBook-Pro:lib mukeshtiwari$ sudo  chmod 755 /usr/local/lib/libyices.2.1.0.dylib
Mukeshs-MacBook-Pro:lib mukeshtiwari$ sudo  ln -sf libyices.2.1.0.dylib /usr/local/lib/libyices.dylib
Mukeshs-MacBook-Pro:lib mukeshtiwari$ sudo  ln -sf libyices.2.1.0.dylib /usr/local/lib/libyices.2.dylib

Mukeshs-MacBook-Pro:~ 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.Yices
Prelude Data.SBV.Bridge.Yices> 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 Yices
***  Executable specified: "yices-smt"


Regards,
Mukesh Tiwari

[1] http://yices.csl.sri.com/download-yices2.shtml


On Mon, Jul 1, 2013 at 2:57 PM, mukesh tiwari <mukeshtiwari.iiitm <at> gmail.com> wrote:
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



_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Johannes Waldmann | 1 Jul 14:34 2013
Picon

Re: Installing Z3 on OS X 10.8.4 ( Off topic )

> Unable to locate executable for z3

well, do you really have z3 in the $PATH?  
what does 'which z3' answer?

I used this for installation of z3:
python scripts/mk_make.py --prefix=/usr/local

and note that the install script says:

Z3 shared libraries were installed at /usr/local/lib, make sure this
directory is in your LD_LIBRARY_PATH environment variable.

- J.W.
Brandon Allbery | 1 Jul 15:42 2013
Picon

Re: Installing Z3 on OS X 10.8.4 ( Off topic )

On Mon, Jul 1, 2013 at 8:34 AM, Johannes Waldmann <waldmann <at> imn.htwk-leipzig.de> wrote:
and note that the install script says:

Z3 shared libraries were installed at /usr/local/lib, make sure this
directory is in your LD_LIBRARY_PATH environment variable.

Only applicable on Linux (and setting the OS X equivalent of LD_LIBRARY_PATH is an absolutely wonderful way to break your system). OS X compiles full paths to shared objects into binaries, and provides a tool to change them if the need arises (install_name_tool).

--
brandon s allbery kf8nh                               sine nomine associates
allbery.b <at> gmail.com                                  ballbery <at> sinenomine.net
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Levent Erkok | 1 Jul 17:02 2013
Picon

Re: Installing Z3 on OS X 10.8.4 ( Off topic )

SBV should be able to pick up Z3 from your path; make sure the "z3" executable is in it and you can invoke it from your shell. Alternatively, you can use the SBV_Z3 environment variable to point to the executable itself, if adding it to your path is not desirable for whatever reason.

Let me know if you still have issues.

-Levent.


On Mon, Jul 1, 2013 at 5:34 AM, Johannes Waldmann <waldmann <at> imn.htwk-leipzig.de> wrote:
> Unable to locate executable for z3

well, do you really have z3 in the $PATH?
what does 'which z3' answer?

I used this for installation of z3:
python scripts/mk_make.py --prefix=/usr/local

and note that the install script says:

Z3 shared libraries were installed at /usr/local/lib, make sure this
directory is in your LD_LIBRARY_PATH environment variable.

- J.W.



_______________________________________________
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
mukesh tiwari | 2 Jul 08:46 2013
Picon

Re: Installing Z3 on OS X 10.8.4 ( Off topic )

Thank you for your response. Now it's working.

-Mukesh Tiwari


On Mon, Jul 1, 2013 at 8:32 PM, Levent Erkok <erkokl <at> gmail.com> wrote:
SBV should be able to pick up Z3 from your path; make sure the "z3" executable is in it and you can invoke it from your shell. Alternatively, you can use the SBV_Z3 environment variable to point to the executable itself, if adding it to your path is not desirable for whatever reason.

Let me know if you still have issues.

-Levent.


On Mon, Jul 1, 2013 at 5:34 AM, Johannes Waldmann <waldmann <at> imn.htwk-leipzig.de> wrote:
> Unable to locate executable for z3

well, do you really have z3 in the $PATH?
what does 'which z3' answer?

I used this for installation of z3:
python scripts/mk_make.py --prefix=/usr/local

and note that the install script says:

Z3 shared libraries were installed at /usr/local/lib, make sure this
directory is in your LD_LIBRARY_PATH environment variable.

- J.W.



_______________________________________________
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


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

Gmane