Am 09.10.2012 um 16:27 schrieb Lawrence Paulson:

> I haven't studied the conditions in detail, but apparently the new licence 
> for Z3 allows redistribution. And I imagine that allows it to be distributed 
> as Isabelle component of sledgehammer.

We already had the explicit permission from the developers to distribute Z3, 
which explains why it's bundled with e.g. Isabelle2012. As before, we still 
cannot enable it without a "Z3_NON_COMMERCIAL" environment variable. Making the 
sources available at all is certainly a step in the right direction for Z3, but 
it doesn't impact us much.

Jasmin

_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to