[isabelle-dev] Towards the Isabelle2014 release

[Makarius]

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 
everything.)

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.

For example:

   lemma "[x] = [y] ⟹ x = y" sledgehammer [prover = smt]
   Sledgehammering...
   "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


 	Makarius