Standard output
721139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
721139 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.5ns
721154 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
721264 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
721264 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
721264 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
721264 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
721671 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
722874 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
724952 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.8s
724952 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
724952 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 441.3ns
724952 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
727547 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s
727563 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
727563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
727563 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns
727563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
730143 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s
730143 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
730143 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.6ns
730143 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
731049 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
732941 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s