Standard output
975190 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
975206 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.1ns
975206 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
975347 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
975347 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
975347 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
975347 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
976136 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
977656 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
980554 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.35s
980554 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
980554 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.07ms
980570 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
984393 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.83s
984409 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
984425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
984425 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.6ns
984425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
988187 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.76s
988187 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
988187 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 445.2ns
988187 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
989408 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
993042 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.86s