From 641a90f1bf6bcc1c7162d6947a2d29ca94bcd09a Mon Sep 17 00:00:00 2001
From: shalashaska117 <72952819+shalashaska117@users.noreply.github.com>
Date: Wed, 29 Jul 2026 14:11:42 +0200
Subject: [PATCH] Fix eqModACRect renaming check and Injectivity success_3
 expectation

eqModAC_ returned early on syntactically identical subterms without
checking them against the renaming it was building up, so two clauses
that shared a subterm could compare equal even when no consistent
renaming existed.

success_3 in tInferences_HOL_Injectivity relied on that. Its expected
clause was copied from success_2, which inverts the first argument of f,
but its input makes f injective in the second. Which clause Injectivity
derives depends on argument evaluation order, because equality arguments
are normalised by term id: clang puts f(X0,X2) on the lhs and derives
inv(X0, f(X0,X2)) = X2, which shares f(X0,X2) with the expectation and
short-circuits. gcc puts f(X0,X1) there, derives inv(X0, f(X0,X1)) = X1,
and fails.

Also fixes the TermList overload of eqModACRect collecting vr from lhs.

Closes #889
---
 Test/TestUtils.cpp                        | 6 ++++--
 UnitTests/tInferences_HOL_Injectivity.cpp | 3 ++-
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/Test/TestUtils.cpp b/Test/TestUtils.cpp
index 41a44ebb4a..f266577061 100644
--- a/Test/TestUtils.cpp
+++ b/Test/TestUtils.cpp
@@ -204,7 +204,9 @@ Stack<TermList> collect(unsigned functor, Term* t) {
 template<class Comparisons>
 bool TestUtils::eqModAC_(TermList lhs, TermList rhs, Comparisons comp)
 {
-  if (lhs == rhs) { return true; }
+  // NB: deliberately no `lhs == rhs` fast path. Two syntactically identical
+  // subterms still have to agree with the renaming `comp` is building up, so
+  // returning early here lets an inconsistent renaming through.
   if (lhs.isVar() && rhs.isVar()) {
     return comp.var(lhs.var(), rhs.var());
   } else if (lhs.isTerm() && rhs.isTerm()) {
@@ -270,7 +272,7 @@ bool TestUtils::eqModACRect(Kernel::TermList lhs, Kernel::TermList rhs)
   auto vl = iterTraits(vi(new VariableIterator(lhs))).collect<Stack>();
   vl.sort();
   vl.dedup();
-  auto vr = iterTraits(vi(new VariableIterator(lhs))).collect<Stack>();
+  auto vr = iterTraits(vi(new VariableIterator(rhs))).collect<Stack>();
   vr.sort();
   vr.dedup();
 
diff --git a/UnitTests/tInferences_HOL_Injectivity.cpp b/UnitTests/tInferences_HOL_Injectivity.cpp
index 3c33090dd2..83d7f5b37e 100644
--- a/UnitTests/tInferences_HOL_Injectivity.cpp
+++ b/UnitTests/tInferences_HOL_Injectivity.cpp
@@ -110,8 +110,9 @@ TEST_GENERATION(success_2,
       .EXPECTED(exactly(clause({ ap(inv(), {z, ap(f, {x, z})}) == x })))
     )
 
+// f is injective in its second argument, so the inverse takes the first
 TEST_GENERATION(success_3,
     Generation::AsymmetricTest()
       .input( clause({ y.sort(srt) == z, ap(f, {x, z}) != ap(f, {x, y}) }))
-      .EXPECTED(exactly(clause({ ap(inv(), {z, ap(f, {x, z})}) == x })))
+      .EXPECTED(exactly(clause({ ap(inv(), {x, ap(f, {x, z})}) == z })))
     )