TestEqualsModProofIrrelevancy

1

tests

0

failures

0

ignored

16.038s

duration

100%

successful

Tests

Test Duration Result
testJavaProof() 16.038s passed

Standard output

1477145    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 
1477145    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.6ns 
1477177    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1477427    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1477427    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1477427    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1477427    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1478349    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
1485312    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.14s 
1485421    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
1486608    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16s 
1486608    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 
1486608    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135ns 
1486624    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1492202    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.59s 
1492264    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
1492906    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 607.8ms