Standard output
1417430 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1417430 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.6ns
1417445 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1417702 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1417702 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1417702 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1417702 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1418739 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1422005 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1427532 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 10.08s
1427532 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1427532 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.4ns
1427532 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1433234 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.71s
1433250 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
1433250 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1433250 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.2ns
1433265 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1438727 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.47s
1438727 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1438727 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.3ns
1438742 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1440621 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1444762 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.03s