Standard output
851778 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
851778 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.1ns
851778 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
851997 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
851997 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
851997 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
851997 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
853099 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
854688 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
857322 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.55s
857337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
857337 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 646.6ns
857337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
860356 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
860371 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
860371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
860371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.4ns
860371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
863721 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s
863737 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
863737 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.3ns
863737 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
864795 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
867146 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s