Standard output
893024 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
893024 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.3ns
893024 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
893180 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
893180 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
893180 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
893180 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
893774 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
895159 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
897958 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.93s
897958 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
897958 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.13ms
897974 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
901628 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s
901690 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
901690 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
901690 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.7ns
901690 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
906107 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.41s
906107 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
906107 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.2ns
906107 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
907342 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
909866 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.75s