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