Standard output
722009 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
722009 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 131ns
722025 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
722134 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
722150 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
722150 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
722150 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
722590 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
723810 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
725930 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.91s
725930 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
725930 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.8ns
725930 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
728671 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s
728671 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
728686 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
728686 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 441.2ns
728686 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
731412 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s
731412 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
731412 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.6ns
731412 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
732365 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
734390 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s