FEDORA-2023-72b3557dee created by jjames a year ago for Fedora 38

Changes in version 4.12.2:

  • remove MSF (Microsoft Solver Foundation) plugin
  • updated propagate-ineqs tactic and implementing it as a simplifier, bound_simplifier. It now eliminates occurrences of "mod" operators when bounds information implies that the modulus is redundant. This tactic is useful for benchmarks created by converting bit-vector semantics to integer reasoning.
  • 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. They are exposed over the SMTLIB API using the command set-simplifier. Simplifiers are similar to tactics, but they operate on solver state that can be incrementally updated. The exposed simplifiers cover all the pre-processing techniques used internally with some additional simplifiers, such as solve-eqs and elim-predicates that go beyond incremental pre-processing used internally. The advantage of using solve-eqs during pre-processing can be significant. Incremental pre-processing simplification using solve-eqs and other simplifiers that change interpretations was not possible before.
  • Optimize added to JS API, thanks to gbagan
  • SMTLIB2 proposal for bit-vector overflow predicates added, thanks to aehyvari
  • bug fixes, thanks to Clemens Eisenhofer, hgvk94, Lev Nachmanson, and others

How to install

Updates may require up to 24 hours to propagate to mirrors. If the following command doesn't work, please retry later:

sudo dnf upgrade --refresh --advisory=FEDORA-2023-72b3557dee

This update has been submitted for testing by jjames.

a year ago

This update's test gating status has been changed to 'ignored'.

a year ago

This update has been pushed to testing.

a year ago

This update has been submitted for stable by bodhi.

a year ago

This update has been pushed to stable.

a year ago

Please login to add feedback.

Content Type
Test Gating
Unstable by Karma
Stable by Karma
Stable by Time
7 days
a year ago
in testing
a year ago
in stable
a year ago
a year ago
BZ#2203492 z3-4.12.2 is available

Automated Test Results