TestEqualsModProofIrrelevancy
Tests
Test |
Duration |
Result |
testJavaProof() |
11.342s |
passed |
Standard output
1148382 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
1148383 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 376.82ns
1148384 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1148647 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1148647 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1148648 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1148648 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1149288 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1153941 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.56s
1154018 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
1154907 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 843.12ms
1154909 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
1154909 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.12ns
1154911 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1159093 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s
1159137 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
1159541 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 373.64ms