Standard output
1111825 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1111825 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.2ns
1111825 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1111981 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1111981 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1111981 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1111981 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1112672 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1114556 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1117926 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.1s
1117942 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1117942 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.4ns
1117942 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1122467 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.53s
1122482 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
1122482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1122482 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.6ns
1122482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1126838 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s
1126838 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1126838 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.5ns
1126838 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1128329 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1131600 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.77s