Standard output
1035418 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1035434 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.61ms
1035434 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1035621 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1035621 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1035621 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1035621 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1036685 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1038529 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1041610 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.18s
1041610 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1041610 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.8ns
1041625 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1045595 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.98s
1045626 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
1045626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1045626 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.9ns
1045626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1049599 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.98s
1049599 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1049599 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.7ns
1049614 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1050975 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1053898 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.29s