Standard output
725406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
725406 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 153ns
725406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
725531 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
725531 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
725531 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
725531 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
725969 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
727235 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
729424 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.01s
729424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
729424 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.9ns
729424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
732208 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
732224 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
732224 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
732224 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.5ns
732224 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
734960 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s
734960 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
734960 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.5ns
734960 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
735929 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
737976 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s