Standard output
1118671 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1118671 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.1ns
1118671 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1118843 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1118843 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1118843 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1118843 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1119581 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1121420 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1124786 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.11s
1124786 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1124786 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.8ns
1124802 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1129312 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.52s
1129327 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
1129327 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1129327 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.7ns
1129327 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1133695 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.38s
1133695 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1133695 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.1ns
1133711 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1135242 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1138605 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.9s