TestEqualsModProofIrrelevancy
Tests
Test |
Duration |
Result |
testJavaProof() |
12.673s |
passed |
Standard output
883872 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
883872 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 170ns
883904 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
884045 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
884045 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
884045 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
884045 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
884563 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
888793 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.9s
889543 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
892617 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3s
892617 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
892617 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.4ns
892632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
895837 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s
895884 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
896310 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 405.53ms