TestEqualsModProofIrrelevancy
Tests
Test |
Duration |
Result |
testJavaProof() |
10.874s |
passed |
Standard output
958256 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
958256 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.9ns
958287 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
958522 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
958522 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
958522 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
958522 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
959085 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
963165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.87s
963275 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
964290 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1s
964290 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
964290 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.3ns
964306 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
968088 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s
968198 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
968902 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 683.48ms