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?
Larry

> 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 MHonArc.