[isabelle-dev] NEWS

Lars Noschinski noschinl at in.tum.de
Mon Jun 4 09:39:53 CEST 2012


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



More information about the isabelle-dev mailing list