Standard output
1147870 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1147870 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.3ns
1147870 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1148105 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1148105 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1148105 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1148105 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1149386 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1151798 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1155520 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.65s
1155551 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1155551 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 579.9ns
1155551 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1160045 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.49s
1160061 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
1160061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1160061 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.4ns
1160061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1164481 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.41s
1164481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1164481 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.3ns
1164481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1166012 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1169334 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.85s