We introduced a constraint on z3 after it has switched the linking mode from static to dynamic. We require the statically linked z3 to build self-contained binary packages, so the easy solution at the time was constraining the version of z3. However, we no longer can survive with the outdated version (especially since we need a newer version of z3 to work with OCaml 5.0, so this issue blocks #1561).
Besides, BAP works fine with either variant of z3 (static or dynamic) so if you want to rebuild bap with the later z3 (assuming you have already bap installed and want to update z3), you can use --ignore-constraints-on, e.g.,
opam install z3=4.8.17 --ignore-constraints-on=z3
And if you're building bap from sources and install bap dependencies with opam install . --deps-only then you can avoid building z3 twice using the following trick:
before installing bap dependencies, install z3 of the desired version, e.g.,
opam install z3=4.8.17
next, use the --ignore-constraints-on=z3 to drop it from the formula and install the dependencies,
We introduced a constraint on z3 after it has switched the linking mode from static to dynamic. We require the statically linked z3 to build self-contained binary packages, so the easy solution at the time was constraining the version of z3. However, we no longer can survive with the outdated version (especially since we need a newer version of z3 to work with OCaml 5.0, so this issue blocks #1561).
Besides, BAP works fine with either variant of z3 (static or dynamic) so if you want to rebuild bap with the later z3 (assuming you have already bap installed and want to update z3), you can use
--ignore-constraints-on, e.g.,And if you're building bap from sources and install bap dependencies with
opam install . --deps-onlythen you can avoid building z3 twice using the following trick:--ignore-constraints-on=z3to drop it from the formula and install the dependencies,