Standard output
864502 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
864502 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.4ns
864502 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
864720 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
864720 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
864720 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
864720 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
865361 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
866815 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
869895 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.4s
869895 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
869895 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.8ns
869911 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
873351 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s
873382 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
873444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
873444 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.6ns
873444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
877057 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s
877057 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
877057 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.4ns
877057 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
878229 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
880841 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s