Standard output
1054722 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1054722 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.7ns
1054722 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1054879 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1054879 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1054879 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1054879 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1055473 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1057302 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1060256 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.54s
1060256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1060256 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 259ns
1060256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1064244 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.98s
1064260 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
1064260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1064260 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.3ns
1064260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1068199 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.94s
1068215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1068215 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.9ns
1068215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1069558 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1072544 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.33s