Standard output
1381550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1381565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.1ns
1381565 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1381831 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1381831 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1381831 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1381831 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1382623 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1385010 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1389403 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.85s
1389419 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1389419 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.7ns
1389419 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1394759 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.35s
1394775 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
1394775 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1394775 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.9ns
1394775 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1400107 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.33s
1400107 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1400107 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.6ns
1400122 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1401928 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1405897 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.79s