Standard output
1337714 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1337714 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.3ns
1337714 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1337996 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1337996 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1337996 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1337996 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1338809 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1340971 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1345058 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.33s
1345058 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1345058 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.4ns
1345058 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1350273 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.21s
1350289 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
1350289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1350289 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.5ns
1350289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1355411 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.12s
1355411 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1355411 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.3ns
1355411 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1357201 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1361077 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.66s