Standard output
1152727 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1152727 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.1ns
1152743 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1152915 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1152915 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1152915 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1152915 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1153776 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1155653 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1158952 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.22s
1158967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1158967 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 935.9ns
1158967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1163351 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.39s
1163367 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
1163383 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1163383 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns
1163383 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1167761 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.37s
1167761 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1167761 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.9ns
1167761 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1169237 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1172503 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.75s