Standard output
1451103 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1451103 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.3ns
1451118 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1451338 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1451338 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1451338 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1451338 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1452183 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1454614 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1459064 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.95s
1459064 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1459064 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.8ns
1459080 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1464662 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.58s
1464662 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
1464662 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1464662 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.1ns
1464678 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1470174 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.5s
1470174 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1470174 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.9ns
1470174 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1472051 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1476186 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.02s