search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
295 stars 51 forks source link

Fixed issue when arg sort to function application is variable #527

Closed joe-hauns closed 8 months ago

joe-hauns commented 8 months ago

This PR fixes a UWA crash in cases where the argument sort to some $app term is a variable.

quickbeam123 commented 8 months ago

Looking good, thanks!

Just a little pause here. Didn't we come to a conclusion it's better now to (temporarily) completely disable HOL vampire, but complaining maybe already in the parser? Isn't it, @MichaelRawson, on your todo list now?

MichaelRawson commented 8 months ago

Yep - but let's have both this and a parser guard so that this is one fewer thing for an eventual HOLy hacker to fix. Do you agree @quickbeam123 ?

quickbeam123 commented 8 months ago

Sure!