Standard output
1083019 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1083019 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 147ns
1083019 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1083175 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1083175 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1083175 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1083175 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1083847 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1085608 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1088755 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.74s
1088771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1088771 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.2ns
1088771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1092970 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.21s
1092990 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
1092990 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1092990 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.5ns
1092990 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1097168 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.19s
1097168 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1097168 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.7ns
1097183 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1098606 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1101709 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.53s