TestEqualsModProofIrrelevancy
Tests
Test |
Duration |
Result |
testJavaProof() |
8.564s |
passed |
Standard output
730745 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
730745 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 801.7ns
730776 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
730901 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
730901 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
730901 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
730901 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
731339 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
734536 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.77s
734601 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
735759 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14s
735759 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
735759 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.2ns
735759 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
738618 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s
738691 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
739161 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 455.27ms