Re: [isabelle] Isabelle2016-1-RC1 sledgehammer "Try this: by presburger" fails



Dear Eugene,

> 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)

Such things happen less and less often, but obviously they still happen.

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

To be able to do anything about it, I must have the possibility to reproduce it. I don't mind if it's a big example -- I can minimize it myself. Would you care to send me your theory files (privately off list)?

I doubt it has anything to do with the 2016-1-RC1 version -- such issues have been around for years -- but I'd look into this, either for the release or after it.

Thanks,

Jasmin





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