z3-4.12.1-bp155.1.6

- update to 4.12.1:
  * change macos build to use explicit reference to Macos version 11. Hosted
    builds are migrating to macos-12 and it broke a user Issue #6539.

- update to 4.12.0
  * move bound_manager to simplifiers, add bound manager to extract_eqs for solve-eqs
  * fix memory leak on proof justifications
  * expose parameters to control behavior for
  * many bugfixes, see https://github.com/Z3Prover/z3/releases

- update to 4.11.2:
  * add error handling to fromString method in JavaScript
  * fix regression in default parameters for CDCL, thanks to Nuno Lopes
  * fix model evaluation bugs for as-array nested under functions (data-type constructors)
  * add rewrite simplifications for datatypes with a single constructor
  * add "Global Guidance" capability to SPACER, thanks to Arie Gurfinkel and Hari Gorvind.
  * change proof logging format for the new core to use SMTLIB commands.
    The format was so far an extension of DRAT used by SAT solvers, but not well compatible
    with SMT format that is extensible. The resulting format is a mild extension of SMTLIB with
    three extra commands assume, learn, del. They track input clauses, generated clauses and deleted clauses.
    They are optionally augmented by proof hints. Two proof hints are used in the current version: "rup" and "farkas".
    "rup" is used whent the generated clause can be justified by reverse unit propagation. "farkas" is used when
    the clause can be justified by a combination of Farkas cutting planes. There is a built-in proof checker for the
    format. Quantifier instantiations are also tracked as proof hints.
    Other proof hints are to be added as the feature set is tested and developed. The fallback, buit-in,
    self-checker uses z3 to check that the generated clause is a consequence. Note that this is generally
    insufficient as generated clauses are in principle required to only be satisfiability preserving.
    Proof checking and tranformation operations is overall open ended.
  The log for the first commit introducing this change contains further information on the format.
  * fix to re-entrancy bug in user propagator (thanks to Clemens Eisenhofer).
  * handle _toExpr for quantified formulas in JS bindings

- update to 4.11.0:
  * remove Z3_bool, Z3_TRUE, Z3_FALSE from the API. Use bool, true, false instead.
  * z3++.h no longer includes <sstream> as it did not use it.
  * add solver.axioms2files
  - prints negated theory axioms to files. Each file should be unsat
  * add solver.lemmas2console
  - prints lemmas to the console.
  * remove option smt.arith.dump_lemmas. It is replaced by solver.axioms2files
  * add option smt.bv.reduce_size.
  - it allows to apply incremental pre-processing of bit-vectors by identifying ranges that are known to be constant.
  This rewrite is beneficial, for instance, when bit-vectors are constrained to have many high-level bits set to 0.
  * add feature to model-based projection for arithmetic to handle integer division.
  * add fromString method to JavaScript solver object.

- update to 4.10.2:
  * fix regression #6194. It broke mod/rem/div reasoning.
  * fix user propagator scope management for equality callbacks.
  * fix implementation of mk_fresh in user propagator for Python API
  * Added API Z3_enable_concurrent_dec_ref to be set by interfaces that
    use concurrent GC to manage reference counts. This feature is integrated
    with the OCaml bindings and fixes a regression introduced when OCaml
    transitioned to concurrent GC. Use of this feature for .Net and Java
    bindings is not integrated for this release. They use external queues
    that are unnecessarily complicated.
  * Added pre-declared abstract datatype declarations to the context so
    that Z3_eval_smtlib2_string works with List examples.
  * Fixed Java linking for MacOS Arm64.
  * Added missing callback handlers in tactics for user-propagator,
    Thanks to Clemens Eisenhofer
  * Tuning to Grobner arithmetic reasoning for smt.arith.solver=6
    (currently the default in most cases). The check for consistency
    modulo multiplication was updated in the following way:
  - polynomial equalities are extracted from Simplex tableau rows using
    a cone of influence algorithm. Rows where the basic variables were
    unbounded were previously included. Following the legacy implementation
    such rows are not included when building polynomial equations.
  - equations are pre-solved if they are linear and can be split
    into two groups one containing a single variable that has a
    lower (upper) bound, the other with more than two variables
    with upper (lower) bounds. This avoids losing bounds information
    during completion.
  - After (partial) completion, perform constant propagation for equalities
    of the form x = 0
  - After (partial) completion, perform factorization for factors of the
    form x*y*p = 0 where x, are variables, p is linear.
  * Added support for declaring algebraic datatypes from the C++ interface.
  * Bugfix release to ensure npm package works
  * Native M1 (Mac ARM64) binaries and pypi distribution.
  - thanks to Isabel Garcia Contreras and Arie Gurfinkel for testing and fixes
  * API for incremental parsing of assertions.
    A description of the feature is given by example here: https://github.com/Z3Prover/z3/commit/815518dc026e900392bf0d08ed859e5ec42d1e43
    It also allows incrementality at the level of adding assertions to the
    solver object.
  * Fold/map for sequences:
    https://microsoft.github.io/z3guide/docs/guide/Sequences#map-and-fold
    At this point these functions are only exposed over the SMTLIB2 interface (and not programmatic API)
    maxdiff/mindiff on arrays are more likely to be deprecated
  * User Propagator:
  - Add functions and callbacks for external control over branching thanks to Clemens Eisenhofer
  - A functioning dotnet API for the User Propagator
    https://github.com/Z3Prover/z3/blob/master/src/api/dotnet/UserPropagator.cs
  * Java Script API
  - higher level object wrappers are available thanks to Kevin Gibbons and Olaf Tomalka
  * Totalizers and RC2
  - The MaxSAT engine now allows to run RC2 with totalizer encoding.
    Totalizers are on by default as preliminary tests suggest this solves already 10% more problems on
    standard benchmarks. The option opt.rc2.totalizer (which by default is true) is used to control whether to use
    totalizer encoding or built-in cardinality constraints.
    The default engine is still maxres, so you have to set opt.maxsat_engine=rc2 to
    enable the rc2 option at this point. The engines maxres-bin and rc2bin are experimental should not be used
    (they are inferior to default options).
  * Incremental constraints during optimization set option opt.incremental = true
  - The interface `Z3_optimize_register_model_eh` allows to monitor incremental results during optimization.
    It is now possible to also add constraints to the optimization context during search.
    You have to set the option opt.incremental=true to be able to add constraints. The option
    disables some pre-processing functionality that removes variables from the constraints.

- Update to 4.8.17
  * fix breaking bug in python interface for user propagator pop
  * Various fixes for z3str3
  * Initial support for nested algebraic datatypes with sequences
  * Initiate map/fold operators on sequences
  * Initiate maxdiff/mindiff on arrays
- Update to version 4.8.16
  * Initial support for Darwin Arm64 (for M1, M2, .. users)
  * Added functionality to user propagator decisions.
  * Added options for rc2 and maxres-bin to maxsat
  * Improved search for mutex constraints (at-most-1 constraints)
    among soft constraints for maxsat derived from approach used
    in rc2 sample.
  * Various other bugfixes

- Update to 4.8.15:
  * Fix solution soundness bug on QF_ABV formula undetected by
    model validator
  * Various other bug fixes

- fix python3-z3 requirement

- update to 4.8.14:
  * fixes Antimirov derivatives for intersections and unions required
  required for solving non-emptiness constraints.
  * includes x86 dll in nuget package for Windows.
  * exposes additional user propagator functionality