Standard output
966561 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
966561 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.9ns
966561 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
966811 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
966811 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
966811 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
966811 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
967749 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
969391 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
972157 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.59s
972157 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
972157 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.2ns
972157 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
975675 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s
975707 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
975707 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
975707 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.8ns
975707 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
979176 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s
979192 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
979192 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 506.3ns
979192 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
980411 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
983038 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.85s