Standard output
1399467 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1399467 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.7ns
1399467 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1399670 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1399670 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1399670 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1399670 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1400501 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1402948 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1407068 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.6s
1407068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1407068 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.8ns
1407081 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1412598 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.52s
1412614 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
1412614 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1412614 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.9ns
1412614 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1417966 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.36s
1417966 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1417966 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.3ns
1417982 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1419757 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1423691 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.72s