Standard output
1333732 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1333732 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.2ns
1333732 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1333967 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1333967 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1333967 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1333967 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1334951 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1338572 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1343684 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 9.95s
1343699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1343699 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.82ms
1343699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1348721 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.02s
1348752 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
1348752 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1348752 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.3ns
1348752 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1353797 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.04s
1353797 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1353797 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 117ns
1353797 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1355517 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1360035 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.23s