Standard output
1062454 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1062454 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.7ns
1062469 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1062610 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1062610 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1062610 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1062610 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1063173 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1065037 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1068171 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.71s
1068171 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1068171 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 470.3ns
1068171 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1072408 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s
1072423 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
1072423 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1072423 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.4ns
1072423 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1076608 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s
1076608 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1076608 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.3ns
1076608 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1078040 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1081100 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.5s