TestEqualsModProofIrrelevancy
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