[isabelle-dev] NEWS

[Sascha Boehme]

Quoting Lars Noschinski <noschinl at in.tum.de>:

> 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?

Z3 is mostly used as backend of Sledgehammer these days. Experiments  
with Sledgehammer indicate that Z3 is capable of solving problems of  
nonlinear arithmetic when multiplication is treated uninterpreted and  
when given enough suitable facts. That is, such an approach increases  
Sledgehammer's overall success rate. However, when resting on the  
interpreted multiplication of Z3, proof reconstruction fails in  
several cases resulting in lost proofs -- something which I consider  
annoying for users. And instead of letting Sledgehammer emit the line

   using [[z3_with_extensions=false]] by (smt fact1 ... factn)

I decided to disable Z3's support for nonlinear arithmetic (and other  
features) by default. Note that you can always recover the original  
behavior by adding this line at the top of your theory:

   declare [[z3_with_extensions]]

Cheers,
Sascha