Standard output
1295902 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1295902 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.1ns
1295902 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1296074 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1296074 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1296074 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1296074 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1296902 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1299079 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1302917 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.01s
1302917 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1302917 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.7ns
1302932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1308239 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.31s
1308255 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
1308255 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1308255 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.2ns
1308255 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1313390 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.15s
1313405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1313405 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.1ns
1313405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1315189 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1319000 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.59s