search

vprover / vampire

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

Well-sortedness check fails during preprocessing in ITP206_4 #602

Open mezpusz opened 1 month ago

mezpusz commented 1 month ago

It should reproduce without any flags. The following assertion is triggered while creating some term in FOOLElimination for a let expression:

Condition in file /Users/mezpusz/vampire/Indexing/TermSharing.cpp, line 178 violated:
_wellSortednessCheckingDisabled || SortHelper::areImmediateSortsValidPoly(t)
Value of t->toString() is: aa(ref(X0),fun(heap_ext(product_unit),product_prod(ref(X0),heap_ext(product_unit))),product_Pair(ref(X0),heap_ext(product_unit)),r21)
mezpusz commented 1 month ago

Same for ITP216_4.