Standard output
1081097 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1081097 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.3ns
1081097 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1081253 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1081253 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1081253 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1081253 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1081940 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1083811 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1087053 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.96s
1087068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1087068 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 487.4ns
1087068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1091340 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s
1091356 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
1091356 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1091356 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 139ns
1091356 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1095539 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.19s
1095539 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1095539 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.2ns
1095539 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1096993 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1100118 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.58s