Re: [isabelle] Bug in Sledgehammer / cvc4



Dear Bohua,

> When I tried sledgehammer on the following theorem:
> 
> theorem Max_ge': "finite A â x > Max A â Â(x â A)"
> 
> The cvc4 output is:
> Try this: using leD by auto (6 ms).
> 
> However, the command does not work. It probably should be
> using Max_ge leD by auto

Thank you for this report. This issue is already fixed in the repository version (since 28 May 2015, right after the release). As a workaround, you can pass the option âdont_minimizeâ to Sledgehammer, e.g.

    sledgehammer [dont_minimize]

when this arises.

Regards,

Jasmin






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