Re: [isabelle] z3
But probably the line was commented out. If the first character is #, delete it (and relaunch Isabelle).
Lawrence C Paulson
Professor of Computational Logic
Computer Laboratory, University of Cambridge
15 JJ Thomson Avenue, Cambridge CB3 0FD, England
Tel: +44(0)1223 334623 Fax: +44(0)1223 334678
On 7 Jan 2014, at 11:06, Roger H. <s57076 at hotmail.com> wrote:
> 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