# Julia bindings for Z3 SMT solver
**URL:** https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218
**Category:** Optimization (Mathematical)
**Created:** [April 26, 2020, 5:36am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218 "2020-04-26T05:36:14Z")
**Posts on this page:** 20
**Page:** 1
### Author:  [@XVilka](https://discourse.julialang.org/u/XVilka)
#### Post date: [April 26, 2020, 5:36am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/1 "2020-04-26T05:36:14Z")
Recently I met the need to access Z3 from Julia program, searched a bit and found abandoned Julia bindings at [zenna/Z3.jl](https://github.com/zenna/Z3.jl). But they do not work with the recent versions and I asked Z3 developers themselves. As it turned out they provide Julia bindings out of the box, just didn’t announce it widely. So for anyone who is going to work with Z3 - see [Julia chapter of their README](https://github.com/Z3Prover/z3#julia). So if anyone wants to test and add an examples - Z3 project welcomes pull requests.
---
### Author:  [@wgm](https://discourse.julialang.org/u/wgm)
#### Post date: [May 1, 2020, 12:11am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/2 "2020-05-01T00:11:29Z")
Thanks for this! We’re you able to get it to compile? I had some issues with cmake.
---
### Author:  [@JeffreySarnoff](https://discourse.julialang.org/u/JeffreySarnoff)
#### Post date: [May 1, 2020, 2:09am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/3 "2020-05-01T02:09:59Z")
It would be wonderful for someone who knows how to make a package that installs the appropriate z3 binary with those Julia extensions and so makes z3 easily available for our use.
---
### Author:  [@thautwarm](https://discourse.julialang.org/u/thautwarm)
#### Post date: [May 1, 2020, 2:23am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/4 "2020-05-01T02:23:05Z")
I’d appreciate in advance if anyone can do this.
---
### Author:  [@viralbshah](https://discourse.julialang.org/u/viralbshah)
#### Post date: [May 1, 2020, 3:09am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/5 "2020-05-01T03:09:52Z")
Would be nice to make it all available as a Julia package and BinaryBuilder!
---
### Author:  [@giordano](https://discourse.julialang.org/u/giordano)
#### Post date: [May 1, 2020, 9:56pm UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/6 "2020-05-01T21:56:25Z")
Z3 is available as a jll package since November: [GitHub - JuliaBinaryWrappers/z3\_jll.jl](https://github.com/JuliaBinaryWrappers/z3_jll.jl) 🙂
---
### Author:  [@giordano](https://discourse.julialang.org/u/giordano)
#### Post date: [May 1, 2020, 11:49pm UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/7 "2020-05-01T23:49:39Z")
Now [`z3_jll`](https://github.com/JuliaBinaryWrappers/z3_jll.jl) has also v4.8.7. However, the Julia bindings are available only in `master`, I’d like to wait to for a new release before building it in Yggdrasil, but maybe you can open an issue to z3 to ask for a new version 😉
---
### Author:  [@JeffreySarnoff](https://discourse.julialang.org/u/JeffreySarnoff)
#### Post date: [May 2, 2020, 12:13am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/8 "2020-05-02T00:13:14Z")
What is the issue that you want to share with Z3?
(please be overly specific, leave nothing to the imagination) 😉
---
### Author:  [@giordano](https://discourse.julialang.org/u/giordano)
#### Post date: [May 2, 2020, 12:30am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/9 "2020-05-02T00:30:00Z")
I mean, you can file a new issue to [GitHub - Z3Prover/z3: The Z3 Theorem Prover](https://github.com/Z3Prover/z3) and encourage the maintainer to release a new version
---
### Author:  [@JeffreySarnoff](https://discourse.julialang.org/u/JeffreySarnoff)
#### Post date: [May 2, 2020, 12:34am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/10 "2020-05-02T00:34:39Z")
Is it that #master has stuff that is ready for release but has not been released? If so, give me one or two items to mention.
---
### Author:  [@giordano](https://discourse.julialang.org/u/giordano)
#### Post date: [May 2, 2020, 12:36am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/11 "2020-05-02T00:36:36Z")
I don’t know z3 at all, the only thing in `master` I know that you could be interested in are the Julia bindings, but I didn’t even looked at how they work 🙂
---
### Author:  [@JeffreySarnoff](https://discourse.julialang.org/u/JeffreySarnoff)
#### Post date: [May 2, 2020, 12:38am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/12 "2020-05-02T00:38:26Z")
ok no problem, same here I will give it shot – after all the Julia bindings should be much easier to build (several of us have tried following the scant directions).
---
### Author:  [@JeffreySarnoff](https://discourse.julialang.org/u/JeffreySarnoff)
#### Post date: [May 2, 2020, 2:56am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/13 "2020-05-02T02:56:31Z")
[issue raised](https://github.com/Z3Prover/z3/issues/4183)
---
### Author:  [@JeffreySarnoff](https://discourse.julialang.org/u/JeffreySarnoff)
#### Post date: [May 2, 2020, 3:23am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/14 "2020-05-02T03:23:57Z")
from Z3:
> we currently build on every commit for the MacOS. The build script is here[(see below):[@ahumenberger](https://github.com/ahumenberger) prepared the script and also created the bindings. He uses a MacOS, so it was easier to create the script for this environment. I am very happy to include CI builds on other platforms, but similar to you, figuring out the magic dependencies is going to take some arm-twisting. If you (or others) can see what should be done for other platforms, say Ubuntu, based on the MacOS script a pull request with an update to the CI pipeline is very welcome. In this way we can build on every push.
[build script](https://github.com/Z3Prover/z3/blob/6088da5159959c099c7b295015cef8aa4887638a/azure-pipelines.yml#L183)
(exerpted)
```julia
- job: "MacOSCMake"
displayName: "MacOS build with CMake"
pool:
vmImage: "macOS-10.14"
steps:
- script: brew install ninja
- script: brew cask install julia
- script: |
julia -e "using Pkg; Pkg.add(PackageSpec(name=\"libcxxwrap_julia_jll\", version=\"0.6.6\"))"
JlCxxDir=$(julia -e "using libcxxwrap_julia_jll; println(joinpath(dirname(libcxxwrap_julia_jll.libcxxwrap_julia_path), \"cmake\", \"JlCxx\"))")
set -e
mkdir build
cd build
CC=clang CXX=clang++ cmake -DJlCxx_DIR=$JlCxxDir -DZ3_BUILD_JULIA_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -DZ3_BUILD_DOTNET_BINDINGS=False -G "Ninja" ../
ninja
ninja test-z3
cd ..
- template: scripts/test-z3.yml
- template: scripts/test-examples-cmake.yml
- template: scripts/test-regressions.yml
```
---
### Author:  [@ahumenberger](https://discourse.julialang.org/u/ahumenberger)
#### Post date: [May 2, 2020, 5:58am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/15 "2020-05-02T05:58:31Z")
As you can see the Julia bindings for Z3 sit on top of the C++ API and use CxxWrap.jl. There is currently a pull request pending which updates the bindings to libcxxwrap 0.7. After that we would need a new release of Z3 to update [z3\_jll](https://github.com/JuliaBinaryWrappers/z3_jll.jl). The package [ahumenberger/Z3.jl](https://github.com/ahumenberger/Z3.jl) would then use z3\_jll.
Right now, ahumenberger/Z3.jl builds an older version of Z3 on the fly. Updating the package to use z3\_jll (once we have new Z3 release) should be easy.
---
### Author:  [@JeffreySarnoff](https://discourse.julialang.org/u/JeffreySarnoff)
#### Post date: [May 2, 2020, 7:51am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/16 "2020-05-02T07:51:37Z")
Thank you. I provided Z3 with those additional [specifics](https://github.com/Z3Prover/z3/issues/4183#issuecomment-622818963).
---
### Author:  [@JeffreySarnoff](https://discourse.julialang.org/u/JeffreySarnoff)
#### Post date: [May 3, 2020, 1:17am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/17 "2020-05-03T01:17:52Z")
for someone who knows who knows and probably @viralbshah:
would you bring the person(s) who know how to help [him do this](https://github.com/Z3Prover/z3/issues/4183#issuecomment-623037533) into that thread
---
### Author:  [@ahumenberger](https://discourse.julialang.org/u/ahumenberger)
#### Post date: [May 12, 2020, 10:01am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/18 "2020-05-12T10:01:42Z")
[Z3.jl v0.4.0](https://github.com/ahumenberger/Z3.jl) is released. It now uses [z3\_jll v4.8.8](https://github.com/JuliaBinaryWrappers/z3_jll.jl). Thanks to everyone involved!
---
### Author:  [@ndinsmore](https://discourse.julialang.org/u/ndinsmore)
#### Post date: [February 13, 2023, 6:38pm UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/19 "2023-02-13T18:38:45Z")
Has anyone been able to run the examples on a Intel Mac? I keep getting a segmentation fault whenever the example tries to create the solver.
---
### Author:  [@Tomas\_Pevny](https://discourse.julialang.org/u/Tomas_Pevny)
#### Post date: [February 19, 2023, 9:16am UTC](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218/20 "2023-02-19T09:16:07Z")
I run into the same issue. A bit frustrating.
[Next page](https://discourse.julialang.org/t/julia-bindings-for-z3-smt-solver/38218.md?page=2)