Standard output
716337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
716337 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.5ns
716337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
716431 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
716431 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
716431 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
716431 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
716853 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
718116 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
720167 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.84s
720167 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
720167 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.9ns
720167 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
722958 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
722958 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
722958 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
722958 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.2ns
722958 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
725714 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s
725714 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
725714 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.8ns
725714 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
726675 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
728668 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s