Standard output
662375 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
662391 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.8ns
662391 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
662454 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
662454 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
662454 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
662454 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
662735 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
663840 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
665824 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s
665824 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
665824 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.7ns
665824 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
668340 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s
668356 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
668356 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
668356 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns
668356 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
670841 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s
670841 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
670841 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns
670841 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
671727 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
673572 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s