From 755d430f24d30f79d3cab1a955ddb3e01aae567b Mon Sep 17 00:00:00 2001
From: Martin Suda <martin.suda@cvut.cz>
Date: Mon, 12 Oct 2026 10:59:20 +0200
Subject: [PATCH] KBO: don't mistake a sort and a term with the same functor
 number for the same symbol

Type constructors and function symbols are numbered independently, so a
sort and a term can share a functor number. KBO::compare (and the
precedence fallback in State::result) only compared the numbers, so e.g.
compare(complex, one_one(complex)) took the lexicographic path over a
0-ary sort and a 1-ary term and returned EQUAL. Cross-kind comparisons
are legitimately made by TermPartialOrdering when ground joinability /
term ordering diagrams relate type and term variables; the bogus EQUAL
made the partial ordering inconsistent and crashed the prover.

Now both places also require the two terms to be of the same kind. This
agrees with PrecedenceOrdering::comparePrecedences (type constructors
below function symbols), which the term ordering diagrams already used,
and makes KBO a consistent order on sorts and terms together.

Reproducer (release build, SIGSEGV after ~5 s before the fix):
  vampire_z3_rel -sa otter Problems/SWV/SWV645_5.p
Unit test KBO/kbo_test24 fails before the fix on ASS(t1->arity()) in
traverseLexBidir.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 Kernel/KBO.cpp     | 14 ++++++++++++--
 UnitTests/tKBO.cpp | 26 ++++++++++++++++++++++++++
 2 files changed, 38 insertions(+), 2 deletions(-)

diff --git a/Kernel/KBO.cpp b/Kernel/KBO.cpp
index 59120faf3..21a355c4a 100644
--- a/Kernel/KBO.cpp
+++ b/Kernel/KBO.cpp
@@ -37,6 +37,16 @@ using namespace std;
 using namespace Lib;
 using namespace Shell;
 
+/**
+ * True if @b t1 and @b t2 have the same top symbol. Type constructors and
+ * function symbols are numbered independently, so a sort and a term can
+ * share a functor number without having anything in common.
+ */
+static bool sameTopSymbol(const Term* t1, const Term* t2)
+{
+  return t1->functor() == t2->functor() && t1->isSort() == t2->isSort();
+}
+
 /**
  * Return result of comparison between @b l1 and @b l2 under
  * an assumption, that @b traverse method have been called
@@ -49,7 +59,7 @@ Ordering::Result KBO::State::result(KBO const& kbo, AppliedTerm t1, AppliedTerm
   Result res;
   if(_weightDiff) {
     res=_weightDiff>0 ? GREATER : LESS;
-  } else if(t1.term.term()->functor()!=t2.term.term()->functor()) {
+  } else if(!sameTopSymbol(t1.term.term(), t2.term.term())) {
     if(t1.term.term()->isLiteral()) {
       ASS(t2.term.term()->isLiteral());
       int prec1, prec2;
@@ -797,7 +807,7 @@ Ordering::Result KBO::compare(AppliedTerm tl1, AppliedTerm tl2) const
 
   state->init();
   Result res;
-  if(t1->functor()==t2->functor()) {
+  if(sameTopSymbol(t1, t2)) {
     res = state->traverseLexBidir(*this, tl1, tl2);
   } else {
     res = state->traverseNonLex</*unidirectional=*/false>(*this, tl1, tl2);
diff --git a/UnitTests/tKBO.cpp b/UnitTests/tKBO.cpp
index 33df7141d..f7e5896c0 100644
--- a/UnitTests/tKBO.cpp
+++ b/UnitTests/tKBO.cpp
@@ -381,6 +381,32 @@ TEST_FUN(kbo_test23) {
   ASS_EQ(ord.compare(f(alpha), g(beta)), Ordering::Result::INCOMPARABLE)
 }
 
+// Type constructors and function symbols are numbered independently, so a sort
+// and a term can share a functor number. KBO::compare used to take that for the
+// same top symbol (seen as compare(complex, one_one(complex)) == EQUAL on SWV645_5).
+TEST_FUN(kbo_test24) {
+  DECL_DEFAULT_SORT_VARS
+  DECL_SORT(pad)
+
+  // pad both symbol tables so that the next type constructor
+  // and the next function symbol get the same number
+  for (unsigned i = 0; env.signature->typeCons() < env.signature->functions(); i++) {
+    TypeConstSugar(("padSort" + Int::toString(i)).c_str());
+  }
+  for (unsigned i = 0; env.signature->functions() < env.signature->typeCons(); i++) {
+    ConstSugar(("padConst" + Int::toString(i)).c_str(), pad);
+  }
+
+  DECL_SORT(srt)
+  DECL_POLY_CONST(one, 1, alpha)
+  ASS_EQ(srt.sugaredExpr().term()->functor(), one.functor())
+
+  auto ord = kbo(weights(), weights());
+
+  ASS_EQ(ord.compare(srt, one(srt)), Ordering::Result::LESS)
+  ASS_EQ(ord.compare(one(srt), srt), Ordering::Result::GREATER)
+}
+
 // isGreater tests
 
 bool isGreaterSymmetric(const KBO& ord, TermList t1, TermList t2) {