Standard output
1397455 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1397455 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.9ns
1397455 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1397658 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1397674 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1397674 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1397674 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1398627 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1400837 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1404872 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.42s
1404872 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1404872 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.6ns
1404888 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1410221 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.34s
1410253 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
1410253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1410253 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.9ns
1410253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1415476 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.23s
1415476 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1415476 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 503.3ns
1415492 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1417289 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1421261 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.78s