Standard output
698877 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
698877 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.8ns
698893 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
698980 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
698980 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
698980 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
698980 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
699481 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
700647 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
702631 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.75s
702631 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
702631 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 520.5ns
702631 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
705314 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s
705329 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
705329 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
705329 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns
705329 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
707998 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s
707998 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
707998 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.8ns
707998 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
708935 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
710898 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s