Email Gateway (Aug 19 2022 at 13:26): Email Gateway (Aug 19 2022 at 13:26):From: "Roger H." <s57076@hotmail.com>
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!
Email Gateway (Aug 19 2022 at 13:26):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Last updated: Apr 19 2024 at 04:17 UTC