Standard output
1331348 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1331348 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 164ns
1331363 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1331582 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1331582 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1331582 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1331582 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1332504 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1334883 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1339112 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.75s
1339112 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1339112 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 810.8ns
1339112 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1344665 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.56s
1344681 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
1344681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1344681 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.8ns
1344697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1350286 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.59s
1350286 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1350286 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.1ns
1350286 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1352173 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1356301 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.01s