TestEqualsModProofIrrelevancy

1

tests

0

failures

0

ignored

20.349s

duration

100%

successful

Tests

Test Duration Result
testJavaProof() 20.349s passed

Standard output

1497676    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 
1497676    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.6ns 
1497692    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1497951    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1497951    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1497951    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1497951    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1498794    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
1508570    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.88s 
1508667    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
1509784    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06s 
1509799    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 
1509799    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189ns 
1509799    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1515665    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.86s 
1516494    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
1517572    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03s