Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

relax the z3 constraint #1568

Open
ivg opened this issue Jan 10, 2023 · 0 comments
Open

relax the z3 constraint #1568

ivg opened this issue Jan 10, 2023 · 0 comments

Comments

@ivg
Copy link
Member

ivg commented Jan 10, 2023

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:

  1. before installing bap dependencies, install z3 of the desired version, e.g.,
opam install z3=4.8.17
  1. next, use the --ignore-constraints-on=z3 to drop it from the formula and install the dependencies,
 opam install . --deps-only --ignore-constraints-on=z3
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant