vprover / vampire

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

Assertion violation with $let sorts #604

Open mezpusz opened 2 months ago

mezpusz commented 2 months ago

Problem

TPTP COM/COM100_5.p

Input

--decode dis-10_1:1_si=on:fdi=16_10

Error

Condition in file Kernel/SortHelper.cpp, line 115 violated:
!subst.isEmpty() || (result.isTerm() && (result.term()->isSuper() || result.term()->ground())) || sym->letBound()

Stack

Kernel::SortHelper::getResultSort(Kernel::Term const*)
Kernel::SortHelper::getResultSortOrMasterVariable(Kernel::Term const*, Kernel::TermList&, Kernel::TermList&)
Kernel::SortHelper::tryGetResultSort(Kernel::Term const*, Kernel::TermList&)
Kernel::SortHelper::tryGetResultSort(Kernel::TermList, Kernel::TermList&)
Kernel::Literal::createEquality(bool, Kernel::TermList, Kernel::TermList, Kernel::TermList)
Inferences::DefinitionIntroduction::introduceDefinitionFor(Kernel::Term*)
Inferences::DefinitionIntroduction::process(Kernel::Term*)
Inferences::DefinitionIntroduction::process(Kernel::Clause*)
Inferences::DefinitionIntroduction::handleClause(Kernel::Clause*, bool)
Indexing::Index::onAddedToContainer(Kernel::Clause*)
Lib::SingleParamEvent<Kernel::Clause*>::MethodSpecificHandlerStruct<Indexing::Index>::fire(Kernel::Clause*)
Lib::SingleParamEvent<Kernel::Clause*>::fire(Kernel::Clause*)
Saturation::AWPassiveClauseContainer::add(Kernel::Clause*)
Saturation::SaturationAlgorithm::addToPassive(Kernel::Clause*)
Saturation::SaturationAlgorithm::doUnprocessedLoop()
Saturation::SaturationAlgorithm::doOneAlgorithmStep()
Saturation::SaturationAlgorithm::runImpl()
Kernel::MainLoop::run()
MichaelRawson commented 2 months ago

555 - thanks for the test-case!