TestEqualsModProofIrrelevancy
Tests
Test |
Duration |
Result |
testJavaProof() |
8.697s |
passed |
Standard output
779748 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
779748 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 210ns
779748 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
779888 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
779888 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
779888 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
779888 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
780420 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
783642 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.9s
783721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
784783 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05s
784783 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
784783 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.8ns
784783 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
787739 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s
787786 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
788270 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 476.09ms