Standard output
1014745 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1014745 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.7ns
1014745 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1014948 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1014948 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1014948 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1014948 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1015581 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1017163 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1020983 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.24s
1020983 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1020983 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 734.8ns
1020983 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1024824 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.83s
1024839 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
1024855 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1024855 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.3ns
1024855 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1029070 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.21s
1029070 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1029070 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 388.5ns
1029070 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1030641 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1033953 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.88s