Standard output
930638 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
930638 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.1ns
930654 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
930812 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
930812 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
930812 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
930812 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
931483 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
933461 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
937640 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.99s
937640 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
937640 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.1ns
937640 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
941240 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s
941256 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
941271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
941271 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.8ns
941271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
944630 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s
944630 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
944630 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.9ns
944630 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
945857 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
948555 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.93s