Standard output
687658 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
687658 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.7ns
687658 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
687758 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
687758 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
687758 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
687758 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
688290 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
689508 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
691525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s
691540 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
691540 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226ns
691540 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
694327 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
694374 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
694389 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
694389 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.8ns
694389 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
697119 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s
697119 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
697119 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.8ns
697135 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
698108 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
700153 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s