Standard output
964131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
964131 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.9ns
964131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
964303 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
964303 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
964303 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
964303 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
965413 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
967101 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
970090 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.96s
970090 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
970090 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 696.5ns
970105 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
973779 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.68s
973810 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
973810 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
973810 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 464.6ns
973810 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
977374 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s
977374 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
977374 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.7ns
977374 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
978703 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
981392 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.02s