Improved heuristics for reasoning about non-linear arithmetic.
Native support for syntax-guided synthesis (sygus).
Support for many new heuristics for reasoning with quantifiers, including
finite model finding.
Support for proofs for uninterpreted functions, arrays, bitvectors, and
their combinations.
Performance improvements to existing theories.
A new theory of sets with cardinality and relations.
A new theory of strings.
Support for unsat cores.
Support for separation logic constraints.
Simplification mode "incremental" no longer supported.
Support for array constants in constraints.
Syntax for array models has changed in some language front-ends.
New input/output languages supported: "smt2.0" and "smtlib2.0" to
force SMT-LIB v2.0; "smt2.5" and "smtlib2.5" to force SMT-LIB v2.5;
"smt2.6" and "smtlib2.6" to force SMT-LIB v2.6;
"smt", "smtlib", "smt2", and "smtlib2" all refer to the current standard
version 2.6. If an :smt-lib-version is set in the input, that overrides
the command line.
Abstract values in SMT-LIB models are now ascribed types (with "as").
In SMT-LIB model output, real-sorted but integer-valued constants are
now printed in accordance with the standard (e.g. "1.0").
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 7 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.