Standard output
851439 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
851439 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.3ns
851439 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
851591 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
851591 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
851591 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
851591 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
852378 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
853924 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
856461 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s
856477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
856477 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 896.4ns
856477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
859738 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s
859759 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
859759 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
859759 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.5ns
859759 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
862976 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s
862992 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
862992 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236ns
862992 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
864102 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
866430 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s