I forgot to patch this part in the latest update; sorry.
This has now been submitted upstream as well.
Originally from dholland@.
Compile-tested on NetBSD/amd64.
Bump PKGREVISION.
From the release notes:
New features:
- New theories of strings and sequences.
- Incremental consequence finder for finite domains.
- CMake build system (thanks @delcypher).
- Updated and improved OCaml API (thanks @martin-neuhaeusser).
- Updated and improved Java API (thanks @cheshire).
- New resource limit facilities to avoid non-deterministic timeout behaviour.
- New bit-vector simplification and ackermannization tactics (thanks @MikolasJanota, @nunoplopes).
- QSAT: a new solver for quantified arithmetic problems. See:
Bjorner, Janota: Playing with Quantified Satisfaction, LPAR 2016.
A multitude of bugs has been fixed.
I am about to commit a separate package for the Python bindings.
Coordinated with dholland@
Fix building math/z3 in privileged mode when not building as root:
ocamlfind: Cannot mkdir /usr/pkg/lib/ocaml/site-lib/Z3: Permission denied
This now uses the option -destdir when calling ocamlfind(1). It also
includes a workaround for what might be a bug in ocamlfind(1), where it
also wants to update ld.conf in spite of specifying -destdir.
Tested on NetBSD/amd64.
ok dholland@
