Standard output
888625 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
888625 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.4ns
888625 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
888769 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
888769 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
888784 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
888784 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
889317 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
890672 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
894079 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.45s
894079 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
894079 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 660.9ns
894095 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
897390 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s
897406 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
897406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
897406 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.6ns
897422 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
900585 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s
900585 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
900585 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 419.9ns
900585 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
901731 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
904131 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.54s