Log message:
py-z3solver: removed, use py-z3 from now on

Log message:
py-z3solver: Portability fixes.

Log message:
python: egg.mk: add USE_PKG_RESOURCES flag

This flag should be set for packages that import pkg_resources
and thus need setuptools after the build step.

Set this flag for packages that need it and bump PKGREVISION.

Log message:
*: bump PKGREVISION for egg.mk users

They now have a tool dependency on py-setuptools instead of a DEPENDS

Log message:
math: Replace RMD160 checksums with BLAKE2s checksums

All checksums have been double-checked against existing RMD160 and
SHA512 hashes

Log message:
math: Remove SHA1 hashes for distfiles

Log message:
py-z3solver: update to version 4.8.9.0

Version 4.8.9
=============
- New features
  - significant improvements to regular expression solving
  - expose user theory plugin. It is a leaner user theory plugin that was once \ 
available.
    It allows for registering callbacks that react to when bit-vector and \ 
Boolean variables
    receive fixed values.
- Bug fixes
  - many
- Notes
  - the new arithmetic theory is turned on by default. It _does_ introduce \ 
regressions on
    several scenarios, but has its own advantages. Users can turn on the old \ 
solver by setting smt.arith.solver=2.
    Depending on feedback, we may turn toggle this default setting again back to \ 
smt.arith.solver=2.

Version 4.8.8
=============
- New features
  - rewritten NIA (non-linear integer arithmetic) core solver
    It is enabled in selected theories as default.
    The legacy arithmetic solver remains the overall default in this release
    as the rewritten solver shows regressions (on mainly NRA problems).
  - recursive function representation without hoisting ite expressions. Issue #2601
  - model-based interpolation for quantifier-free UF, arithmetic
  - Julia bindings over the C++ API, thanks to ahumenberger
- Bug fixes
  - numerous, many based on extensive fuzz testing.
    Thanks to 5hadowblad3, muchang, numairmansur, rainoftime, wintered
- Notes
  - recursive functions are unfolded with separate increments based on unsat core
    analysis of blocking literals that are separate for different recursive \ 
functions.
  - the seq (string) solver has been revised in several ways and likely shows some
    regressions in this release.

Version 4.8.7
=============
- New features
  - setting parameter on solver over the API by
    solver.smtlib2_log=<filename>
    enables tracing calls into the solver as SMTLIB2 commands.
    It traces, assert, push, pop, check_sat, get_consequences.
- Notes
  - various bug fixes
  - remove model_compress. Use model.compact
  - print weights with quantifiers when weight is != 1

Version 4.8.6
=============
- Notes
  - various bug fixes
  - built in support for PIP, thanks to Audrey Dutcher
  - VS compilation mode including misc flags for managed packages

Version 4.8.5
=============
- Notes
  - various bug fixes

Version 4.8.4
=============

- Notes
  - fixes bugs
  - a substantial update to how the seq theory solver handles regular
    expressions. Other performance improvements to the seq solver.
  - Managed .NET DLLs include dotnet standard 1.4 on supported platforms.
  - Windows Managed DLLs are strong signed in the released binaries.

Version 4.8.3
=============
- New features
  - Native handling of recursive function definitions, thanks to Simon Cruanes
  - PB rounding based option for conflict resolution when reasoning about PB \ 
constraints.
  - Access to numeral constants as a double from the native API.

- Notes
  - fixes several bugs discovered since the 4.8.1 release.

Version 4.8.2
=============
- Post-Release.

Version 4.8.1
=============
- Release. Bug-fix for 4.8.0

Version 4.8.0
=============

- New requirements:
  - A breaking change to the API is that parsers for SMT-LIB2 formulas return a \ 
vector of
    formulas as opposed to a conjunction of formulas. The vector of formulas \ 
correspond to
    the set of "assert" instructions in the SMT-LIB input.

- New features
   - A parallel mode is available for select theories, including QF_BV.
     By setting parallel.enable=true Z3 will spawn a number of worker threads \ 
proportional to the
     number of available CPU cores to apply cube and conquer solving on the goal.
   - The SAT solver by default handle cardinality and PB constraints using a \ 
custom plugin
     that operates directly on cardinality and PB constraints.
   - A "cube" interface is exposed over the solver API.
   - Model conversion is first class over the textual API, such that subgoals \ 
created from running a
     solver can be passed in text files and a model for the original formula can \ 
be recreated from the result.
   - This has also led to changes in how models are tracked over tactic \ 
subgoals. The API for
     extracting models from apply_result have been replaced.
   - An optional mode handles xor constraints using a custom xor propagator.
     It is off by default and its value not demonstrated.
   - The SAT solver includes new inprocessing techniques that are available \ 
during simplification.
     It performs asymmetric tautology elimination by default, and one can turn \ 
on more powerful inprocessing techniques
     (known as ACCE, ABCE, CCE). Asymmetric branching also uses features \ 
introduced in Lingeling by exploiting binary implication graphs.
     Use sat.acce=true to enable the full repertoire of inprocessing methods. By \ 
default, clauses that are "eliminated" by acce are tagged
     as lemmas (redundant) and are garbage collected if their glue level is high.
   - Substantial overhaul of the spacer horn clause engine.
   - Added basic features to support Lambda bindings.
   - Added model compression to eliminate local function definitions in models when
     inlining them does not incur substantial overhead. The old behavior, where \ 
models are left
     uncompressed can be replayed by setting the top-level parameter \ 
model_compress=false.
   - Integration of a new solver for linear integer arithmetic and mixed linear \ 
integer arithmetic by Lev Nachmanson.
     It incorporates several improvements to QF_LIA solving based on
     . using a better LP engine, which is already the foundation for QF_LRA
     . including cuts based on Hermite Normal Form (thanks to approaches described
       in "cuts from proofs" and "cutting the mix").
     . extracting integer solutions from LP solutions by tightening bounds \ 
selectively.
       We use a generalization of Bromberger and Weidenbach that allows avoiding \ 
selected
       bounds tightenings (https://easychair.org/publications/paper/qGfG).
     It solves significantly more problems in the QF_LIA category and may at \ 
this point also
     be the best solver for your problem as well.
     The new solver is enabled only for select SMT-LIB logics. These include \ 
QF_LIA, QF_IDL, and QF_UFLIA.
     Other theories (still) use the legacy solver for arithmetic. You can enable \ 
the new solver by setting
     the parameter smt.arith.solver=6 to give it a spin.

- Removed features:
  - interpolation API
  - duality engine for constrained Horn clauses.
  - pdr engine for constrained Horn clauses. The engine's functionality has been
    folded into spacer as one of optional strategies.
  - long deprecated API functions have been removed from z3_api.h

Version 4.7.1
=============

- New requirements:
  - uses stdbool and stdint as part of z3.

- New features:
  - none

- Removed features:
  - none

- Notes:
   This is a minor release prior to a set of planned major updates.
   It uses minor version 7 to indicate that the use of stdbool and
   stdint are breaking changes to consumers of the C-based API.

Version 4.6.0
=============

- New requirements:
  - C++11 capable compiler to build Z3.
  - C++ API now requires C++11 or newer.

- New features (including):
  - A new string solver from University of Waterloo
  - A new linear real arithmetic solver
  - Changed behavior for optimization commands from the SMT2 command-line interface.
    Objective values are no longer printed by default. They can be retrieved by
    issuing the command (get-objectives). Pareto front objectives are accessed by
    issuing multiple (check-sat) calls until it returns unsat.

- Removed features:
  - Removed support for SMT-LIB 1.x

Log message:
Fix vector to element array conversion