Fix eqModACRect renaming check and Injectivity success_3 expectation

[shalashaska117]

Fixes #889.

TestUtils::eqModAC_ opened with

if (lhs == rhs) { return true; }

On shared terms that is pointer equality, and it returned without recording the variable renaming, so eqModACRect accepted clause pairs that are not equal up to renaming whenever the two happened to share a subterm.

success_3 in tInferences_HOL_Injectivity was riding on that. Its input makes f injective in its second argument, so the left inverse is inv(x, f(x,z)) = z, but the expectation was copied from success_2 and says inv(z, f(x,z)) = x. Which clause Injectivity derives depends on the evaluation order of the two operands of !=, because equality arguments are normalised by term id. clang derives inv(X0, f(X0,X2)) = X2, which shares f(X0,X2) with the expectation and short-circuits, so CI stayed green. gcc derives inv(X0, f(X0,X1)) = X1, and the test fails.

Three changes:

• Drop the fast path in eqModAC_.
• Correct the success_3 expectation.
• Fix the TermList overload of eqModACRect, which collected vr from lhs and so compared lhs against itself in its variable count guard. Nothing in the suite goes through that overload, so it is a separate bug I noticed while reading rather than something this PR needed.

Checked with gcc 15.2, Debug: 97/97 in about 20s, unchanged from before, so no other test was relying on the fast path.

With the fast path gone the old expectation also fails under clang's ordering. I reproduced that ordering under gcc by swapping the written order of the two operands, which builds the same clause but reverses the creation order:

[     case ]: { X1 = X2 | ~(f @ X0 @ X2 = f @ X0 @ X1) }
[       is ]: [ { inv_f_0 @ X0 @ (f @ X0 @ X2) = X2 } ]
[ expected ]: exactly: [ { inv_f_0 @ X2 @ (f @ X0 @ X2) = X0 } ]
[ FAIL ] success_3

---

Disclosure: I used AI to generate this PR text. The code has been wrote by myself.

[mezpusz]

The tests are seemingly not slowed down by the removed check, so I approve. Thanks for the fix!

[mezpusz]

This should also fix the coverage build, rerunning now 🤞 https://github.com/vprover/vampire/actions/runs/30460258799