Standard output
735016 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
735016 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.9ns
735016 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
735119 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
735119 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
735119 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
735119 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
735612 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
736918 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
739083 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s
739098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
739098 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.1ns
739098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
741876 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
741892 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
741907 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
741907 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.6ns
741907 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
744714 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
744714 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
744714 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.8ns
744730 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
745693 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
747780 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s