TestEqualsModProofIrrelevancy

1

tests

0

failures

0

ignored

12.673s

duration

100%

successful

Tests

Test Duration Result
testJavaProof() 12.673s passed

Standard output

883872     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 
883872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170ns 
883904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
884045     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
884045     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
884045     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
884045     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
884563     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
888793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.9s 
889543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
892617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3s 
892617     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 
892617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.4ns 
892632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
895837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
895884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0 
896310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 405.53ms