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
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
