Standard output
1387706 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1387706 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.6ns
1387722 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1387925 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1387925 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1387925 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1387925 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1388889 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1391151 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1395221 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.5s
1395221 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1395221 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.6ns
1395221 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1400605 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.38s
1400605 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
1400605 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1400605 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.5ns
1400621 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1405965 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.36s
1405965 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1405965 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 198ns
1405981 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1407802 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1411856 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.88s