TestEqualsModProofIrrelevancy
Tests
Test |
Duration |
Result |
testJavaProof() |
7.771s |
passed |
Standard output
686880 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
686880 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.6ns
686895 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
686989 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
687005 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
687005 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
687005 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
687329 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
690324 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s
690371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
691449 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06s
691449 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
691449 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 106ns
691449 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
694044 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s
694075 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
694513 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 419.11ms