vprover/vampire

Parse errors for polymorphic problems

ibnyusuf opened this issue · 4 comments

When parsing invalid polymorphic syntax (TFF and particularly TFX) parser fails in unexpected ways with poor or no error messages.

Could you give an example problem, @ibnyusuf ? I have completely forgotten the context for this so it would be good to know when it is fixed or what still needs fixing.

Sorry, I should have recorded this when I opened the issue! Unfortunately, I have now totally forgotten what syntactic errors trigger crashes in the parser.

I reckon that introducing syntax errors into valid benchmarks should lead to crashes pretty soon.

No problem! I think I found some the other day by randomly running through TPTP so I'll do that again and post some here.

In #542, Joe picked some up. Let's say that they were these.