Standard output
920461 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
920461 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.1ns
920461 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
920617 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
920617 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
920617 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
920617 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
921227 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
922790 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
925669 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.21s
925669 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
925669 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 643.8ns
925684 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
929108 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s
929139 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
929139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
929139 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.1ns
929139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
932563 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s
932563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
932563 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 421.9ns
932563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
933736 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
936348 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.77s