TestEqualsModProofIrrelevancy
Tests
Test |
Duration |
Result |
testJavaProof() |
13.675s |
passed |
Standard output
898730 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
898746 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.08ms
898777 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
898917 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
898917 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
898917 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
898917 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
899449 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
903378 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.61s
904551 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
908251 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.66s
908251 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
908251 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 457ns
908251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
911581 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s
911643 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Relaxed[Relaxed::isRelaxedPrefix([I,[I)].JML operation contract.0
912206 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 556.05ms