vprover / vampire

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

FOOL constant symbol assertion violation #606

Open mezpusz opened 2 months ago

mezpusz commented 2 months ago

Benchmark

TPTP SYO/SYO015^1.p

Options

-newcnf on

Error

Condition in file Kernel/Formula.hpp, line 361 violated:
env.signature->isFoolConstantSymbol(false, functor)

Stack

Kernel::BoolTermFormula::create(Kernel::TermList)
Shell::Flattening::innerFlatten(Kernel::Formula*)
Shell::Flattening::flatten(Kernel::Formula*)
Shell::Flattening::innerFlatten(Kernel::Formula*)
Shell::Flattening::flatten(Kernel::Formula*)
Shell::Flattening::flatten(Kernel::FormulaUnit*)
Shell::Preprocess::preprocess1(Kernel::Problem&)
Shell::Preprocess::preprocess(Kernel::Problem&)
preprocessProblem(Kernel::Problem*)
doProving(Kernel::Problem*)
vampireMode(Kernel::Problem*)
dispatchByMode(Kernel::Problem*)
main
MichaelRawson commented 2 months ago

This is HOL, shouldn't we error for this?

ibnyusuf commented 2 months ago

It is one of those wierd problems that are marked as higher-order, but actually contain no higher-order features.