Standard output
721035 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
721035 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.2ns
721035 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
721145 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
721145 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
721145 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
721145 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
721551 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
722802 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
724992 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.95s
724992 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
724992 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.01ms
724992 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
727727 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s
727743 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
727758 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
727758 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.3ns
727758 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
730447 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s
730463 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
730463 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.6ns
730463 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
731401 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
733402 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s