TestEqualsModProofIrrelevancy

1

tests

0

failures

0

ignored

13.736s

duration

100%

successful

Tests

Test Duration Result
testJavaProof() 13.736s passed

Standard output

1276265    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 
1276265    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.1ns 
1276296    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1276531    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1276531    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1276531    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1276531    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1277516    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
1282790    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.5s 
1282884    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
1284009    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09s 
1284009    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 
1284009    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 474ns 
1284009    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1288999    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 
1289061    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
1289718    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 625.65ms