Re: [isabelle] Isabelle2016-1-RC1 sledgehammer "Try this: by presburger" fails
Iâm afraid that such things do happen from time to time. I also get meson proofs that only succeed if metis is substituted. Still some bugs in there clearlyâ but who could live without it?
> On 8 Nov 2016, at 08:49, Eugene W. Stark <isabelle-users at starkeffect.com> wrote:
> In Isabelle2016-1-RC1 I am seeing instances where sledgehammer
> says, for example:
> "cvc4": Try this: by presburger (24 ms)
> "z3": Try this: by presburger (16 ms)
> "spass": Try this: by presburger (20 ms)
> But attempting to use "by presburger" fails.
> In such cases, "by metis" succeeds.
> I don't know if that is enough of a clue as to where to look.
> I am not sure how to abstract an example of this. Is there
> another way I can supply the necessary information?
> - Gene Stark
This archive was generated by a fusion of
Pipermail (Mailman edition) and