[isabelle-dev] NEWS: Z3 open source
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?
More information about the isabelle-dev