Standard output
1338773 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1338773 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.4ns
1338773 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1338992 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1338992 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1338992 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1338992 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1339883 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1342181 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1346058 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.28s
1346074 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1346074 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.8ns
1346074 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1351249 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.18s
1351280 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
1351280 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1351280 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 846.3ns
1351280 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1356439 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.16s
1356454 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1356454 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.6ns
1356454 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1358174 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1362019 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.56s