Standard output
1088032 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1088032 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.5ns
1088032 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1088188 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1088204 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1088204 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1088204 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1088805 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1090769 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1094169 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.14s
1094169 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1094185 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 782.2ns
1094185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1098696 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.51s
1098696 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
1098711 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1098711 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.7ns
1098711 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1103200 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.49s
1103200 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1103200 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.9ns
1103200 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1104764 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1108029 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.82s