Crash on `PUZ091^5` with NewCNF

[MichaelRawson]

% Running in auto input_syntax mode. Trying TPTP
Condition in file /home/michael/vampire/Shell/NewCNF.cpp, line 1139 violated:
term->isSpecial()
Value of term->toString() is: cEARNEST
----- stack dump -----
Version : Vampire 4.8 (commit aa47c04cf on 2024-05-16 12:10:57 +0100)
call stack: 0x42a101 0x7f9971046305 0x7f997104624a 0x42e16d 0x42cb00 0x42ba5e 0x42a3dd 0x42a319 0xa4b85f 0xa4ca94 0x8fbb4b 0x8fc230 0x90441a 0x4b4a96 0x43b611
invoking addr2line(1) ...
_start
??:?
??
??:0
??
??:0
main
/home/michael/vampire/vampire.cpp:795
dispatchByMode(Kernel::Problem*)
/home/michael/vampire/vampire.cpp:560
vampireMode(Kernel::Problem*)
/home/michael/vampire/vampire.cpp:366
doProving(Kernel::Problem*)
/home/michael/vampire/vampire.cpp:150
preprocessProblem(Kernel::Problem*)
/home/michael/vampire/vampire.cpp:131
Shell::Preprocess::preprocess(Kernel::Problem&)
/home/michael/vampire/Shell/Preprocess.cpp:283
Shell::Preprocess::newCnf(Kernel::Problem&)
/home/michael/vampire/Shell/Preprocess.cpp:623
Shell::NewCNF::clausify(Kernel::FormulaUnit*, Lib::Stack<Kernel::Clause*>&)
/home/michael/vampire/Shell/NewCNF.cpp:78
Shell::NewCNF::process(Kernel::Formula*, Shell::NewCNF::Occurrences&)
/home/michael/vampire/Shell/NewCNF.cpp:1276
Shell::NewCNF::processBoolterm(Kernel::TermList, Shell::NewCNF::Occurrences&)
/home/michael/vampire/Shell/NewCNF.cpp:1139
void Debug::Assertion::violated<std::__cxx11::basic_string<char, std::char_traits<char>, Lib::STLAllocator<char> > >(char const*, int, char const*, std::__cxx11::basic_string<char, std::char_traits<char>, Lib::STLAllocator<char> > c
onst&, char const*)
/home/michael/vampire/Debug/Assertion.hpp:240
Debug::Tracer::printStack(std::ostream&)
/home/michael/vampire/Debug/Tracer.cpp:51
----- end of stack dump -----

Perhaps somebody with NewCNF or HOL expertise knows what's going on.

[quickbeam123]

@ibnyusuf has to confirm, but I don't think NewCNF could at any time read HOL.

[MichaelRawson]

Right - I thought we USER_ERRORed with "NewCNF doesn't HOL yet" at some point in the relatively-recent past. But seems not, maybe we should put it back.

[MichaelRawson]

Ahah. We still do - try a "proper HOL" problem, and we bail out before CNF transformations with "Vampire is not HOLy". However PUZ091^5 is written in the THF dialect but it's actually a FOOL problem with no higher-order part at all, so Vampire continues and crashes another way somehow - does NewCNF support FOOL in principle?

[MichaelRawson]

On closer inspection it's not even FOOL - just propositional!