Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] "~~/src/HOL/Tools/ATP/atp_problem.ML": unexpec...

view this post on Zulip Email Gateway (Jul 19 2022 at 11:52):

From: Peter Lammich <lammich@in.tum.de>
When running sledgehammer with vampire, I get an "unexpected term in
first-order format" exception, somewhere from the internals of the
problem encoding.

Example for reproduction attached
Bug1.thy

view this post on Zulip Email Gateway (Jul 19 2022 at 14:27):

From: "\"Blanchette, J.C. (Jasmin Christian)\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi Peter,

I cannot reproduce the bug with a recent repository version (707748d3d186). We fixed quite a few Sledgehammer bugs in the last few months, so it's plausible that it's gone. If you can reproduce it with a repository version, please let me know (or post it to the -dev mailing list).

Cheers,
Jasmin

Last updated: Jan 04 2025 at 20:18 UTC