New Feature: Support for optimization queries. The SMT-LIB2 command language is augmented by three commands (maximize <expr>), (minimize <expr) and (assert-soft <expr> [:weight <numeral>] [:id <identifier>]). The programmatic API also contains a dedicated context for solving optimization queries. The TACAS 2015 tool paper by Bjorner, Dung and Fleckenstein describes additional details and the online tutorial on http://rise4fun.com/z3opt illustrates some uses.
How to install
Updates may require up to 24 hours to propagate to mirrors. If the following command doesn't work, please retry later:
This update has been submitted for testing by jjames.
This update has been pushed to testing.
This update has reached 3 days in testing and can be pushed to stable now if the maintainer wishes
This update has been submitted for stable by jjames.
This update has been pushed to stable.