Z3-4.8.8 was released with many bugfixes since 4.8.6 (currently in the tree): https://github.com/Z3Prover/z3/releases/tag/z3-4.8.8 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
https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=4a8053a105372c6eaf0a11c42681602b8fb20f67 Was already done by time you posted bug, it seems.
