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> wrote:

> Hi,
> 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?
> Thanx!

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