Standard output
1434857 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1434857 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.1ns
1434857 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1435076 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1435076 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1435076 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1435076 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1436045 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1438390 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1442598 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.74s
1442598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1442598 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.1ns
1442613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1448305 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.7s
1448336 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
1448336 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1448336 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.3ns
1448336 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1453840 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.5s
1453840 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1453840 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.8ns
1453840 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1455669 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1459781 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.94s