Standard output
702449 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
702465 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 98ns
702465 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
702559 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
702559 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
702559 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
702559 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
703023 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
704249 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
706361 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.9s
706361 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
706361 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 188ns
706361 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
709124 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s
709124 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
709124 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
709124 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns
709124 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
711855 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s
711855 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
711855 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.5ns
711871 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
712829 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
714831 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s