Standard output
821476 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
821476 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 175ns
821476 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
821617 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
821617 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
821617 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
821617 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
822120 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
823779 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
826069 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.6s
826069 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
826085 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 897.5ns
826085 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
829232 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s
829250 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
829250 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
829250 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.6ns
829250 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
832293 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s
832293 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
832293 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.4ns
832293 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
833346 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
835978 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.68s