[isabelle-dev] NEWS: Z3 open source

Makarius makarius at sketis.net
Thu Apr 9 21:25:15 CEST 2015


On Wed, 8 Apr 2015, Jasmin Blanchette wrote:

>  - Z3 is now always enabled by default, now that it is fully open
>    source. The "z3_non_commercial" option is discontinued.
>
> In addition, Z3 should now (again) be invoked by default by 
> Sledgehammer. Let me know if you see anything odd, e.g. odd problems 
> with binaries on Linux or Windows.

Great.  I have seen this in the vicinity of 1e3383a5204b.

Can you explain the status of Old_SMT?  Is there anything that isatest 
still needs to run here?


 	Makarius




More information about the isabelle-dev mailing list