TestEqualsModProofIrrelevancy

1

tests

0

failures

0

ignored

10.874s

duration

100%

successful

Tests

Test Duration Result
testJavaProof() 10.874s passed

Standard output

958256     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 
958256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.9ns 
958287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
958522     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
958522     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
958522     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
958522     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
959085     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
963165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.87s 
963275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
964290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1s 
964290     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 
964290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.3ns 
964306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
968088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 
968198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
968902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 683.48ms