Standard output
1013498 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1013498 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.5ns
1013498 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1013733 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1013733 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1013748 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1013748 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1014815 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1016597 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1019583 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.09s
1019598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1019598 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.9ns
1019598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1023211 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.62s
1023242 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
1023242 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1023242 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.1ns
1023242 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1026887 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s
1026887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1026887 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.9ns
1026887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1028153 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1030779 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.89s