Standard output
1111433 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1111433 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.8ns
1111433 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1111621 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1111621 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1111621 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1111621 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1112309 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1114249 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1117494 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.07s
1117494 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1117510 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 771.8ns
1117510 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1121783 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s
1121798 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
1121798 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1121798 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns
1121798 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1126036 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.23s
1126036 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1126036 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.4ns
1126036 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1127455 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1130647 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.61s