Standard output
894491 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
894491 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.9ns
894491 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
894647 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
894647 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
894647 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
894647 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
895263 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
896659 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
899722 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.23s
899722 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
899722 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.7ns
899722 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
903029 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s
903045 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
903045 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
903045 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.9ns
903045 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
906329 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s
906329 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
906329 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.5ns
906344 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
907814 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
911441 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s