Re: [isabelle] Sledgehammer: One-line proof reconstruction failed [still happening in RC2]



Hi Jasmin,

> I am glad to report that the source of the problem appears to have
> been identified and eradicated (see change 20af2ad9261e if you're 
> using the development version).

I've found another instance of this problem in RC2. All of these work:

"cvc4": One-line proof reconstruction failed: by (smt subsetI).
"z3": Timed out.
"spass": One-line proof reconstruction failed: by (metis subset_code(1)).
"e": One-line proof reconstruction failed: by (metis subsetI).
"remote_vampire": One-line proof reconstruction failed: by (metis subsetI).

It's in a bigger theory context this time. I can send you my files if
you want.

Cheers
Lars




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