Standard output
856314 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
856314 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 143ns
856314 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
856439 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
856439 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
856439 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
856439 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
857075 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
858404 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
860952 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.64s
860952 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
860952 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.6ns
860952 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
864438 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s
864798 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
864798 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
864798 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.3ns
864798 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
868878 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s
868878 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
868878 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.1ns
868878 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
870003 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
872356 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s