[isabelle-dev] "spass": Internal error: exception Empty raised (line 458 of "library.ML")

[Alexander Krauss]

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"