Standard output
850837 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
850837 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.4ns
850837 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
850998 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
850998 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
850998 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
850998 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
851663 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
853760 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
856477 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.64s
856477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
856477 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 687ns
856493 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
860035 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s
860098 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
860098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
860098 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 106ns
860114 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
867484 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.38s
867484 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
867484 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.6ns
867499 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
868734 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
871387 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.9s