TestEqualsModProofIrrelevancy

1

tests

0

failures

0

ignored

7.771s

duration

100%

successful

Tests

Test Duration Result
testJavaProof() 7.771s passed

Standard output

686880     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 
686880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.6ns 
686895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686989     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
687005     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
687005     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
687005     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
687329     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
690324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
690371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
691449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06s 
691449     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 
691449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106ns 
691449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
694044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
694075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
694513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 419.11ms