TestEqualsModProofIrrelevancy

1

tests

0

failures

0

ignored

13.675s

duration

100%

successful

Tests

Test Duration Result
testJavaProof() 13.675s passed

Standard output

898730     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 
898746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.08ms 
898777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
898917     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
898917     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
898917     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
898917     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
899449     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
903378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.61s 
904551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
908251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.66s 
908251     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 
908251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 457ns 
908251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
911581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
911643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
912206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 556.05ms