Standard output
871578 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
871578 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.4ns
871578 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
871705 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
871705 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
871705 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
871705 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
872213 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
873557 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
876352 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.77s
876352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
876352 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.9ns
876352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
879700 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s
879715 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
879715 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
879715 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.2ns
879715 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
882995 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s
882995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
882995 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 408.7ns
882995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
884151 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
886652 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s