Re: [isabelle] Bug in Sledgehammer / cvc4
> 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.
when this arises.
This archive was generated by a fusion of
Pipermail (Mailman edition) and