Re: [isabelle] Isabelle2016-RC0: cvc4 crashing

> On 14.01.2016, at 20:43, Eugene W. Stark <isabelle-users at> wrote:
> I will see what I can do, but it is not deterministically repeatable,
> and I usually just invoke sledgehammer by typing "try" or "try0".

I see. Then I recommend you instead add

    sledgehammer_params [overlord]

somewhere upstream (e.g. at the top of your file or in a theory file all your other theory files depend on). This will also affect "try".

Be aware that this option is not thread-safe -- i.e. if you have several Sledgehammers running at the same time somehow (e.g. several jEdits running), the problem or proof files might overwrite each other. Which is not the end of the world. I have never run into problems myself and use this option often (hence its name ;)), but I thought I'd mention this.


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