[isabelle] z3


by using sledgehammer, i get this:

"z3": A prover error occurred:
The SMT solver Z3 is not activated. To activate it, set
the environment variable "Z3_NON_COMMERCIAL" to "yes",
and restart the Isabelle system.
See also "/cygdrive/c/Users/DRaco/Desktop/Work/Isabelle2013-1/contrib/z3-3.2/etc/settings" 

I went to settings and "Z3_NON_COMMERCIAL" was already set to "yes".
What now?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.