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) {