TestEqualsModProofIrrelevancy
Tests
Test |
Duration |
Result |
testJavaProof() |
20.349s |
passed |
Standard output
1497676 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
1497676 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.6ns
1497692 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1497951 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1497951 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1497951 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1497951 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1498794 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1508570 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 10.88s
1508667 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
1509784 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06s
1509799 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
1509799 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 189ns
1509799 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1515665 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.86s
1516494 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
1517572 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03s