[isabelle-dev] NEWS

[Lars Noschinski]

On 04.06.2012 09:28, Sascha Boehme wrote:
> The SMT solver Z3 has now by default a restricted set of directly
> supported features. For the full set of features (div/mod, nonlinear
> arithmetic, datatypes/records) with potential proof reconstruction
> failures, enable the configuration option "z3_with_extensions". Minor
> INCOMPATIBILITY.

What is the reasoning behind this change?

   -- Lars