z3-4.5.0+git.20170523-2.1

- Update cmake parameters

- Update to version 4.5.0+git.20170523:
  * update readme
  * ignore Z3-str source
  * failing test case: SMT2 parse string constants
  * create and register string theory plugin the parser gets a little bit further now! rejects input with "unexpected character"
  * fix string constant representation in parser spec1 loopback OK
  * pretty-printing of string constants in AST spec2 looks good now
  * load str decl plugin; recognize String sorted constants
  * register Concat function now reaches str_decl_plugin::mk_func_decl()
  * at least for now, Concat is no longer associative this means that we'll always have (Concat a b) instead of variadic forms
  * add Length function to theory of strings
  * AND MUCH MORE...

- Z3Config.cmake is not needed anymore
- Update to version 4.5.0+git.20170313:
  * Fixed utf-8 version string handling for python2. Resolved #787
  * Set soname version correctly in cmake build
  * cmake build: set SOVERSION to include the minor version number
  * fix overflow exposed in #880
  * Thread labels through tactic system
  * Add basic Sine Qua Non filtering
  * adding parallel threads
  * Fix off-by-one bug in array indexing in the OCaml bindings
  * refine parsat
  * add const &
  * Introduce and use labels_vec
  * ensure that parallel threads are only invoked when thread count > 1
  * add name
  * delete comment
  * delete unused args
  * reindent
  * use insert_if_not_there
  * fix issues with running parallel solver: random strategy should not be a default on all solvers. Also reuse base solver
  * fix bug in propagation of parameters to combined solvers
  * bypass combined solver when logic is set to QF_BV or QF_FD
  * bypass combined solver when logic is set to QF_FD
  * move exchange par
  * enable pb theory always as pb terms can be introduced during transformations. Issue #884
  * use is_uninterp
  * correctly pretty-print
  * add and use new is_pattern recognizer
  * add par_or tactic to C++ API. #873
  * fix bug in lexicographic handling in maxres: previous assumptions were not committed in corner cases
  * Fixed signed/unsigned warnings
  * Fixed model-converter segfault in ::check_sat. Relates to #881
  * Fixed model-converter segfault in ::check_sat. Relates to #881
  * add itos/stoi conversion to API. Issue #895
  * fix model generation for non-linear expressions, reported by Martin Suda and Giles Reger
  * expose numerator/denominators for Martin and Giles
  * add missing mod/rem/is_int functionality to C++ API
  * make parameters accessible from expressions. Issue #896
  * add par_and_then
  * use non _ method from z3printer module so to be resilient against how _ is handled as indicator of private functions
  * add recursive function graphs to model, adapt rewriter to bypass branches whose evaluation is redundant
  * add octal escape to seq_decl_plugin
  * C-style octal escapes, including 1- and 2-digit escapes
  * add _re.unroll internal operator to seq_decl_plugin
  * expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911
  * expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911
  * remove unreferenced label
  * fix type on exception message
  * fix unhandled finite domain sort rewrite case. Issue #918
  * Java API for getting the objective value as a triple
  * Sane indentation + removing extra spaces for Optimize.java
  * Class Optimize#Handle should be static,
  * fixed bug where `mk_make.py --build=...` would fail to handle absolute paths correctly.
  * Free allocated char arrays in JNI API
  * [CMake] For single configuration generators only allow `CMAKE_BUILD_TYPE` to be one of the pre-defined build configurations that we support.
  * add boolean operators to zstring and fix ostream
  * Tabs, whitespace
  * fix bug for bit-vector optimization. Issue #919
  * fix bug for bit-vector optimization. Issue #928
  * ensure evaluation of array equalities is enabled for external facing evaluator. Issue #917
  * check that formulas are in lira before invoking qsat. Issue #919
  * add notes to README based on feedback in #916
  * remove scratch notes from readme
  * include recursive functions to models. Issue #898
  * remove print breaking build
  * fixing build break, adding fixedpoint object to C++ API
  * adding fixedpoint object to C++ API
  * fixing build break, addressing #935
  * z3py: With tactical should not try to use context as a parameter
  * move restore relevancy until after literals have been replayed
  * [CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git's HEAD so that the necessary code is rebuilt when the build system is invoked.
  * [CMake] Implement generation of `Z3Config.cmake` and `Z3Target.cmake` file for the build and install tree.
  * [CMake] Python examples should only be copied over if python bindings are being built.
  * [CMake] Build `c_example`, `cpp_example` and `z3_tptp5` as external projects.
  * [CMake] Fix typo handling OpenMP flags.
  * [CMake] Fix examples linking against libz3 when it is built as a static library on Linux.
  * [CMake] On Windows when building the examples copy the Z3 library into the directory of the example executable so that it works "out of the box".

- add Z3Config for cmake

- Update to version 4.5.0+git.20170126:
  * streamline logging in arithmetic
  * adding preferred sat, currently disabled, to wmax. Fixing issue #815
  * make a few functions static
  * remove 2 outdated comments
  * add a few more statics to avoid symbol clashes
  * Re-added context creation locks in the Java API. Relates to #819.
  * Bugfix for model construction. Fixes #828.
  * adding range to C API. Issue #831
  * add range constructor to .NET API
  * add regular expression operations to C and C++ API
  * add regular expression features to C# API
  * add missing complement
  * add python API for newly exposed regex constructors
  * exposing regular expression features to address issue #831
  * produce error message for cores with optimization. Issue #825
  * Whitespace
  * Bugfix for special-case handling in fp.fma.
  * fix bug in encoding of axioms for indexof. Issue #806
  * Bugfix for special-case handling in fp.fma.
  * Build fix for C++ example
  * add virtual destructors, fix operator code for API methods complement and intersection per note by Loris d'Antoni
  * address #835
  * address #835
  * address warnings from #836
  * add virtual destructor to intermediary class in case this helps for #835
  * address other warnings per input from delcypher
  * bail out on failure to properly project
  * bail out on failure to properly project. issue #837
  * remove nested booleans during pre-processing. issue #837
  * add suggestions from #835
  * fix bug in handling of repeated soft constraints. #815
  * Add rewrite rule for property encoded in #812
  * Fix implementation of `scoped_timer` under Linux where it was incorrectly assumed that `pthread_cond_timedwait()` would exit due to a condition variable being signaled or a timeout occuring.
  * handle model generation from issue #748. Deal with warnings from #836
  * Build fix for C/C++ example programs.
  * Style, whitespace.
  * ensure that FD logic understands pb from command context
  * Making z3 python look in its installation directory for the z3 lib
  * fix generation of wcnf
  * Build fix for static binaries + shared examples
  * Fix for parallel builds of the OCaml API. Relates to #797.
  * Fix inconsistent emission of OCaml enumeration files. The ordering of emitted enum values is not consistent between python 2 or 3. The root cause of the problem was a dictionary's keys being iterated over which has no defined order.
  * Refactor `mk_z3consts_ml()` code into `mk_z3consts_ml_internal()` and move that into `mk_genfile_common.py`. Then adapt `mk_util.py` and `mk_consts_files.py` to call into the code at its new location.
  * Refactor `update_api.mk_ml()` so that the source and output directories can be different. This feature will be needed by the CMake build system to build the OCaml bindings.
  * Fix issue with bd1f07f864a7f1790cec08a306ccc17507f7e5a8 pointed out by @nunolopes .
  * remove sources for unused variable warnings
  * fix debug build, unused variable warnings
  * fix build again
  * Add -fpic to armv7/armv8 build
  * updated encodings
  * remove redundant disjunction in compilation of at-most-1 constraints, log mutexes
  * fix missing else reported in #855
  * improve parser error message over API, streamline names of statistics for arithmetic solver
  * add restart.max parameter to control cancellation based on restart count
  * initialize watch in assign_eh
  * make get_consequence call skip check-sat if a model is already there
  * enable incremental consequence finding with restart timeout
  * Fixed initialization order warning.
  * add operator for issue #860
  * allow disabling exceptions from C++. Issue #861
  * moderate exception behavior for issue #861
  * fix bug in antecedent collection for consequence finding: once an antecedent is set, it should not be cleared
  * add at-least and pbge to API, fix for issue #864
  * remove polynomial factorization as suggested by issue #852
  * Removed polynomial factorization test cases. Relates to #852 and fixes #865.
  * GCC compilation/keyword fix. Relates to #864
  * update CMakeList to remove polynomial-factorization
  * Formatting, whitespace
  * Added option to extend unsat cores with literals that (potentially) provide quantifier instances.
  * Cleaned up #include<iostream> in api* objects.
  * Formatting, whitespace, and Z3_API annotations.
  * Bugfix for smt.core.extend_patterns
  * Omit '.dll' from library name for DllImport.
  * Mark void DummyContracts as Conditional to avoid compiling their arguments.
  * Corner-case fix for smt::solver::pop_core
  * Update README.md
  * remove unused features related to weighted check-sat
  * Added win64 build badge
  * Separated win32/64 builds
  * Added MAKEJOBS env var to mk_unix_dist.py
  * Fix unsound handling of upper bounds in wmax, thanks to Patrick Trentin for report and careful repros #847
  * use stirngs for env variables
  * fix crash with unary xor #870
  * fix memory leaks from cancellations
  * update macro_util logging to uniform format
  * build fix
  * Added (include ...) SMT2 command.
  * Added filenames to error messages for when we have more than one file.
  * Enabled filenames in error messages during inclusion of files.
  * Updated cmake build
  * Windows build fix.
  * Bugfix for macro finder. Fixes #832.
  * fix bug in consequence extraction: the order of bcp is not fixed between restarts, so the order of unit literals may not be preserved. This is relatively rare, so we optimize for the case where we assume bcp preserves order (and maybe miss some consequences)
  * Another fix for  #847. Reset wmax theory solver state between lex calls, otherwise it uses stale constraints
  * Added .NET 3.5 solution/project files
  * x64 build fix for .NET 3.5 API
  * Windows build fix.
  * access parameters from Python API
  * Added option to limit the distance of unsat core extension through patterns.
  * fix test for int-value
  * fix regression for z3num
  * fix bug in sat-simplifier decreasing heap values of variables that are not in the heap
  * fix part 1 of #875
  * add warning for scearios of #876
  * add format #879
  * rework sat.mus to use restart count for bounded minimization

- Update to version 4.5.0+git.20161129:
  * remove legacy interface to dt2bv tactic
  * Fixed potential problems with invalidated iterators.
  * Fix for previous commit.
  * whitespace
  * Silenced GCC warning about empty loop body.
  * local
  * fix mutex finding for smt-core: it was returning mutexes for negations of literals
  * Bugfixes for the FPA  API
  * fix at-most-1 constraint compiler bug
  * fix at-most-1 constraint compiler bug
  * add bounded-int and pb2bv solvers to fd_solver, use sorting networks for pb2bv rewriter when applicable, hoist to pb2bv_rewriter module and remove it from the pb2bv_tactic
  * add example to exercise at-most-1 constraints
  * add documentation
  * add missing file
  * disable local optimization in presence of non-linear constraints, addresses issue #758
  * whitespace
  * Added accessors to extract sign/exponent/significand BV numerals from FP numerals.
  * Added functions to test FP numerals for special values.
  * Fixed FP numeral special value sig/exp extraction functions.
  * Resolved rebase conflicts
  * Refactored FPA numeral accessors.
  * Replaced antiquated header with modern equivalent.
  * removed unused variables
  * fixed GCC build issue in tests
  * a more efficient encoding for pseudo-Boolean inequality constraints into bit-vectors
  * merge
  * fix incorrect assertion when checking signs of literals, exposed by mitls regressions
  * fix incorrection assertion when checking signs of literals, exposed by miTLS regressions
  * remove dead (and incorrect) code
  * add handling of pseudo-boolean inequalities that use if-expressions over Booleans and arihmetic instead of built-in PB predicates
  * fix sign of constant in pb constraint
  * removed debug output
  * fix for biased flag on get_numeral_exponent_string
  * fix for Python API installation
  * fixed initialization order warning in pb2bv_rewriter
  * fixed unhandled case warning in test/qe_arith.cpp
  * additional robustness check for incremental sat solver core when it recieves interpreted constants, added PB equality to interface and special handling of equalities to adddress performance gap documented in #755
  * fix unit tests for pb
  * disabled unnecessary assertion
  * Bugfix for Python API.
  * Marked .NET Z3Exception as serializable
  * Fixed FPA unbiased exponent accessors
  * Bugfix for bv2fpa_converter. Fixes #767.
  * Added FPA numeral predicates to .NET API
  * Added FPA numeral predicates to Java API
  * Added FPA numeral predicates to ML API
  * remove conflict on false disequality, introduced regression
  * Added Z3_fpa_is_numeral_negative to FPA API
  * Added is_numeral_negative to .NET and Java APIs
  * Added FPA numeral accessors/predicates to Python API
  * speed up consequence finding by avoiding local search whenver assumption level is reached during the initial phase
  * fix enum2bv to handle singleton enumeration types, differentiate disequality conflicts for theories that handle disequalities vs. theories that don't
  * rewind qhead to ensure re-propagation after cancellation
  * catch cancellation exceptions, return undef
  * fixing cancellation code paths for inc_sat_solver
  * removed debug output
  * Build fix for libz3.vcxproj.
  * whitespace
  * Bugfix for bouned_int2bv_solver
  * ensure that variables passed to consequence finding have bound constraints, if applicable. Even if those variables do not occur in the constraints
  * merge
  * fix performance bottlnecks: gc of literals walk through potentially huge watch-lists, avoid user-push/pop around calls to solver2tactic
  * fix memory abuse in internalization in inc-sat-solver
  * remove buggy and unused equivalence relation plugin. Github issue #770
  * disable sat solver when proofs are turned on. Fixes issue #768
  * fix bug in mutex extraction, reported by Patrick Trentin
  * build fix
  * bugfix for disequality propagation in smt_context
  * enable unsat core extraction in nlsat_tactic
  * Fixes for .NET Core build
  * fixing unsat core extraction for tactics
  * fix evaluator for array store expressions
  * remove recursive expansion of else-case
  * fixed log output typo
  * Added signed .NET assemblies in unix builds
  * Whitespace
  * Disabled some ITE rewrite rules that were applied by default, but too expensive. Added re-computation of subterm occurrences in ctx_simplify_tactic. (Performance fixes for QF_LIA benchmarks).
  * check for logic in solver
  * fix generation of fresh constants for uninterpreted sort in EPR, Issue #649
  * Added release notes for the upcoming 4.5.0 release
  * fix crash in poly normalizer exposed by qe. Issue #775
  * Updated optimization ML API. Addresses #776.
  * Whitespace, typo
  * eliminated unnecessary variable
  * fix breaking change to theory-seq
  * Whitespace
  * Whitespace
  * updated release notes
  * added is_numeral_negative to ML API.
  * FPA API clarification
  * Bugfix for denormal numeral exponents
  * build fix
  * bugfix for macro finder
  * detect quantifiers in model expressions to quiet down failing model validation
  * Include Python API files in distributions.
  * Bumped version to 4.5.0
  * Standardize on __uint64 instead of unsigned __int64
  * Bumped version number.
  * [CMake] Bump the version number in the CMake build.
  * fixed hard-coded version number in setup.py
  * Whitespace
  * Typo
  * Bugfix for Z3_fpa_get_numeral_*_uint64. Relates to #570.
  * Bugfix for Z3_fpa_get_numeral_sign. Relates to #570.
  * typo
  * fix crash reported in #784
  * Fixed problems with aborted rewriters in theory_fpa. Relates to #570.
  * Fix cleanup/initialization of sat::simplifier. Relates to #570.
  * Fixed compiler warning
  * Fixed interruption cleanup bug in sat_solver. Relates to #570.
  * Fixed potential SAT solver cleanup problem. Renamed functions for consistency. Relates to #570.
  * fix lexicographic combinations for wmax: pb constrsaints were not interpreted in Boolean benchmarks. #782
  * make semantics of extract/substr deterministic. Issue #781
  * Fixed Windows distribution script.
  * Bugfix for rewriter exceptions in theory_fpa. Relates to #570.
  * Assertion fix for theory_fpa. Relates to #570.
  * improving perf of mutex finding, revert semantics of 0 timeout to no-timeout. Issue #791
  * fix perf bug reported in #790
  * Fixed interruption/cancelation issue in rewriter.
  * Cleaned up hacky rewriter cancelation fix in theory_fpa.
  * fix and coallesce clique functionality
  * tune initialization for wmax and sortmax
  * fix bug incorrect clearing of goals during node creation. Issue #777
  * fix unsoundness reported in issue #777, disable ematching on recursive function definition axioms exposed in #793
  * Fix GCC/Clang compilation.
  * fix crash in new clique code
  * re-enable ematching on recursive function definitions, disabling ematching breaks regressions
  * Fix for the documentation scripts. Fixes #799.
  * Added optional synchronization for multi-thread API logs. Relates to #798.
  * Fixed OpenMP problems in log synchronization. Relates to #798.
  * fix handling of AC operator ++ on regular expressions. Issue #804
  * fix warnings in configure script
  * Do not request time stamp if not needed
  * Fixed iterator invalidation bug in SAT probing. Relates to #798.
  * optimize pattern matching code generator for DAG patterns generated code now uses COMPARE instructions to compare subtrees instead of diving into both subtrees. Code is thus smaller and fails faster.
  * small optimization in compilation of multi-patterns also make the path faster for single patterns
  * mam compiler: move reset of matched_exprs cache next to code reset
  * blast distinct in incremental BV solver

- Update to version 4.4.1+git.20161018:
  * adding enumeration tests
  * spacing, unit test
  * Bugfix for bv2fpa (model) conversion.
  * Removed unnecessary variables.
  * [CMake] Fix building the Java bindings.
  * adding unit test for enumeration types
  * Tabs
  * undo breaking commit
  * Whitespace
  * Fixed iterator invalidation bug in theory_arith_nl.
  * add fd solver for finite domain queries
- remove link-against_libs.patch

- make -devel require libz3, not z3
- add link-against_libs.patch

- Update to version 4.4.1+git.20161007:
  * Z3_query_constructor documentation clarification
  * add mutex pass
  * Build/test fix for python3
  * Test fix for python3
  * Added dummy code contracts for .NET Core/CoreCLR builds.
  * Remove unnecessary "unsafe" qualifier on internal .NET API class.
  * add mutex preprocessing to maxsat, add parsing functions to C++ API
  * add example of parsing with external declarations
- Speedup build by using ninja

- Update to version 4.4.1+git.20160914:
  * addressing max-segment issue for AMD64 + Debug
  * safe sat clause_offset in debug mode
  * safe sat clause_offset in debug mode
  * fixes to consequence generation and cancellation
  * move from uint_set to hashtable over unsigned to save memory overhead in consequence generation
  * ensure stoi axiom even when no value is present for argument. Issue #731
  * add missing rewrite rule. Issue #731
  * fix heisenbug, unintialized variable, issue #720
  * add patch to deal with bug exposed in issue #721
  * fix regression in seq-replace rewriting
  * ensure that status is displayed in SMT-LIB2 compliant way. Issue #734
  * Create socrates.py
  * remove special characters
  * Update socrates.py
- Rename python bindnigs to follow openSUSE guidelines
- Change _service to disabled to avoid unnecessary executions
- Small packaging changes

- Update descriptions

- Update to version 4.4.1+git.20160717:
  * fix bugs exposed in #677. to_int(x) has the semantics that to_int(x) <= x, and to_int(x) is the largest integer satisfying this inequality. The encoding in purify_arith had it the other way x <= to_int(x) contrary to how to_int(x) is handled elsewhere. Another bug in theory_arith for mixed-integer linear case was also exposed. Fractional bounds on expressions of the form to_int(x), and more generally on integer rows were not rounded prior to internalization
  * garbage collect all api::object references when calling del_context. Request issue #679
  * add proper garbage collection to ast_manager. Issue #679
  * remove unfinished ite-macro finder, tune ast GC to ensure nodes are roots only once
  * fix rounding mode for pseudo-boolean constraint creation, Issue #683
  * add object z3 objects to target context during translation, to fix build regression failure on z3test.py
  * add tptp5 example to cmake, adding output SZS directives for Geoff
  * fix ubuntu build failure
  * mark also ast in parameters as GC roots. Issue #676
- Use cmake macros
- Some spec file polishing with spec-cleaner

- update to 20160717
  * a lot of changes, see the repo
- remove CMake-Provide-a-way-to-customise-the-install-directo.patch
- add remove-timestamp.patch

- disable build of examples (unused)

- update to 20160309
- remove: 0001-cmake-add-base-files.patch (not needed anymore)
- add CMake-Provide-a-way-to-customise-the-install-directo.patch
- correct packaging

- initial package

- update to 4.12.2
  * remove MSF (Microsoft Solver Foundation) plugin.
  * updated propagate-ineqs tactic and implementing it as a simplifier,
    bound_simplifier.
  * add API function Z3_mk_real_int64 to take two int64 as arguments. The
    Z3_mk_real function takes integers.
  * Add _simplifiers_ as optional incremental pre-processing to solvers.
  * Optimize added to JS API.
  * SMTLIB2 proposal for bit-vector overflow predicates added.
  * bug fixes.
- add 0001-Fix-building-with-gcc-13-6723.patch

- 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