TestEqualsModProofIrrelevancy
Tests
Test |
Duration |
Result |
testJavaProof() |
13.736s |
passed |
Standard output
1276265 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
1276265 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.1ns
1276296 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1276531 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1276531 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1276531 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1276531 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1277516 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1282790 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.5s
1282884 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
1284009 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09s
1284009 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
1284009 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 474ns
1284009 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1288999 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s
1289061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
1289718 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 625.65ms