TestEqualsModProofIrrelevancy

1

tests

0

failures

0

ignored

8.564s

duration

100%

successful

Tests

Test Duration Result
testJavaProof() 8.564s passed

Standard output

730745     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 
730745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 801.7ns 
730776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
730901     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
730901     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
730901     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
730901     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
731339     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
734536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.77s 
734601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
735759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14s 
735759     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 
735759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.2ns 
735759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
738618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
738691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
739161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 455.27ms