Standard output
722708 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
722708 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.1ns
722708 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
722817 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
722817 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
722817 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
722817 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
723255 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
724490 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
726647 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.94s
726663 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
726663 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 613.9ns
726663 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
729368 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s
729392 INFO Test worker d.u.i.k.s.n.ContractLoadingTests self.sumAndMax(a) catch(exc)
pre: ( \forall int i;
( (0 <= i & i < a.length)<<SC>> & inInt(i)
-> 0 <= a[i])
& ((self.<inv><<impl>> & (!a = null)<<impl>>)<<SC>>))<<SC>>
post: (\forall int i;
( (0 <= i & i < a.length)<<SC>> & inInt(i)
-> a[i] <= self.max)
& (( ( a.length > 0
-> \exists int i;
(( (0 <= i
& i < a.length)<<SC>>
& inInt(i)
& self.max = a[i])<<SC>>))
& (( self.sum = bsum{int i;}(0, a.length, a[i])
& (( self.sum <= a.length * self.max
& self.<inv><<impl>>)<<SC>>))<<SC>>))<<SC>>))<<SC>>
& (exc = null)<<impl>>
mod: {(self, SumAndMax::$sum)}
\cup {(self, SumAndMax::$max)}
termination: diamond
729392 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
729392 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.7ns
729392 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
732073 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s
732073 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
732073 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.7ns
732073 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
733026 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
734998 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s