TestEqualsModProofIrrelevancy
Tests
Test |
Duration |
Result |
testJavaProof() |
8.660s |
passed |
Standard output
742812 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
742812 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.1ns
742828 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
743000 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
743000 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
743000 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
743000 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
743605 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
746685 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.85s
746747 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
747873 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1s
747873 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
747873 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.9ns
747873 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
750751 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s
750798 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
751267 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 460.62ms