EqualsModProofIrrelevancy might not be properly working

[tobias-rnh]

Description

While working on some things in keyext.rusty I was taking a look at EqualsModProofIrrelevancy in key.util to see where it is used and how it works. The test class for EqualsModProofIrrelevancy looks like the following:

class TestEqualsModProofIrrelevancy {
    public static final File testCaseDirectory = FindResources.getTestCasesDirectory();

    @Test
    void testJavaProof() throws Exception {
        KeYEnvironment<DefaultUserInterfaceControl> env =
            KeYEnvironment.load(new File(testCaseDirectory,
                "../../../../../key.ui/examples/heap/verifyThis15_1_RelaxedPrefix/relax.proof"));
        Assertions.assertNotNull(env.getLoadedProof());
        Assertions.assertTrue(env.getLoadedProof().closed());
        KeYEnvironment<DefaultUserInterfaceControl> env2 =
            KeYEnvironment.load(new File(testCaseDirectory,
                "../../../../../key.ui/examples/heap/verifyThis15_1_RelaxedPrefix/relax.proof"));
        Assertions.assertNotNull(env2.getLoadedProof());
        Assertions.assertTrue(env2.getLoadedProof().closed());

        Proof proof1 = env.getLoadedProof();
        Proof proof2 = env.getLoadedProof();

        // compare some proof nodes
        for (int i = 0; i < proof1.countNodes(); i += 15) {
            int serialNr = i;
            Node node1 = proof1.findAny(n -> n.serialNr() == serialNr);
            Node node2 = proof2.findAny(n -> n.serialNr() == serialNr);
            Assertions.assertNotNull(node1);
            Assertions.assertNotNull(node2);
            for (int j = 1; j <= node1.sequent().size(); j++) {
                SequentFormula sf1 = node1.sequent().getFormulabyNr(j);
                SequentFormula sf2 = node2.sequent().getFormulabyNr(j);
                Assertions.assertTrue(sf1.equalsModProofIrrelevancy(sf2));
            }
            if (node1.getAppliedRuleApp() != null) {
                Assertions.assertTrue(
                    node1.getAppliedRuleApp().equalsModProofIrrelevancy(node2.getAppliedRuleApp()));
            }
        }
        env.dispose();
        env2.dispose();
    }
}

What stood out to me was that proof1 and proof2 are both initialized with the proof from env, instead of using env2 for proof2.
Is it supposed to be like this, or should env2 be used to initialize proof2?
Because applying the change results in the test not passing on my machine.

Reproducible

always

Steps to reproduce

1. Use env2 instead of env in the line Proof proof2 = env.getLoadedProof();
2. Run the test
3. Test fails

Additional information

I also see another potential problem in the implementation of equalsModProofIrrelevancy in TacletApp.java with one if statement:

  if ((missingVars != null || !that.missingVars.isEmpty())
          && (!missingVars.isEmpty() || that.missingVars != null)
          && !Objects.equals(missingVars, that.missingVars)) {
      return false;
  }

Judging by the checks for null, it should be possible that missingVars and that.missingVars are both null, which would cause a NullPointerException in the first line. It would also be possible to get a NullPointerException in the second line.
Does a scenario not occur where a NullPointerException can be thrown?

• Commit: 144a9ba