[isabelle-dev] Towards the Isabelle2014 release
makarius at sketis.net
Mon Jul 7 11:38:43 CEST 2014
On Mon, 7 Jul 2014, Mamoun FILALI-AMINE wrote:
> I have downloaded the Isabelle2014-RC0, the smt solver is not anymore
> implicitely in the window of solvers and when we put it it gives up
> systematically, please is there some setting to do?
(I am bouncing this back on the mailing list, since I am not the expert of
You probably mean the defaults for the "Provers" in the Sledgehammer
panel. It is now a bit simpler in only providing some static default,
which is made persistent on the editor side if you change that.
Adding "smt" there includes that prover, but by default the main SMT
solver Z3 is not activated, and somehow its invokation via Sledgehammer
does not inform the user about it.
lemma "[x] = [y] ⟹ x = y" sledgehammer [prover = smt]
"smt": The prover gave up.
Here is the user-relevant message, produced in a different way:
lemma "x = x" by smt
The SMT solver Z3 is not activated. To activate it, set the Isabelle
system option "z3_non_commercial" to "yes"
(e.g. via the Isabelle/jEdit menu Plugin Options / Isabelle / General).
See also http://z3.codeplex.com/license
More information about the isabelle-dev