Standard output
1019911 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1019911 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.8ns
1019911 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1020052 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1020068 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1020068 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1020068 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1020708 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1022381 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1025305 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.38s
1025305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1025305 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 475.3ns
1025305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1029244 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.94s
1029275 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
1029275 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1029275 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.5ns
1029275 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1033230 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.96s
1033230 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1033230 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.1ns
1033230 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1034559 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1037482 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s