TestEqualsModProofIrrelevancy

1

tests

0

failures

0

ignored

8.660s

duration

100%

successful

Tests

Test Duration Result
testJavaProof() 8.660s passed

Standard output

742812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\..\..\..\..\..\key.ui\examples\heap\verifyThis15_1_RelaxedPrefix\relax.proof 
742812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.1ns 
742828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743000     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
743000     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
743000     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
743000     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
743605     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
746685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.85s 
746747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
747873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1s 
747873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\..\..\..\..\..\key.ui\examples\heap\verifyThis15_1_RelaxedPrefix\relax.proof 
747873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.9ns 
747873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
750798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
751267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 460.62ms