Re: [isabelle] Sledgehammer: veriT in Isabelle 2019

I downloaded and built veriT but couldn’t get it to prove the simplest theorem within sledgehammer. As I recall, the documentation says that sledgehammer was only tested on the 2014 version. I suspect it isn’t worth bothering with.


> On 4 Oct 2019, at 14:18, Randy Pollack <rpollack at> wrote:
> The Isabelle 2019 Sledgehammer document says:
>         If you installed an official Isabelle package, it should
> already include
>         properly setup executables for CVC4, E, SPASS, Vampire, veriT, and Z3,
>         ready to use.
> Indeed CVC4, E, SPASS, Vampire and Z3 work like a champ, but I can't
> figure out verit:
> "No such prover: verit" (also   "No such prover: veriT").  I'm using a
> download of the Isabelle2019 package on MacOs  10.14.6.  Everything
> else seems to work.
> Thanks for any help,
> --Randy

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.