Hi,
I just got the following internal error from spass while trying out the
monolithic Windows bundle from Makarius:
theory Scratch
imports Main
begin
lemma "A ⟶ B ⟹ A ⟹ B"
sledgehammer
Sledgehammering...
"spass": Internal error:
exception Empty raised (line 458 of "library.ML")
"remote_vampire": Try this: by metis (12 ms).
"remote_e_sine": Try this: by metis (13 ms).
"e": Try this: by metis (14 ms).
"z3": A prover error occurred:
The SMT solver Z3 is not activated. To activate it, set
the environment variable "Z3_NON_COMMERCIAL" to "yes".
See also
"/cygdrive/c/Users/alexander.krauss/Downloads/Isabelle_23-Apr-2012/contrib/z3-3.2/etc/settings"
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
