diff --git a/Test/TestUtils.cpp b/Test/TestUtils.cpp
index 41a44ebb4..f26657706 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 3c33090dd..83d7f5b37 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 })))
     )