Standard output
1320860 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1320860 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.4ns
1320860 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1321032 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1321032 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1321032 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1321032 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1321860 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1324214 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1328077 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.21s
1328077 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1328077 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.7ns
1328077 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1333235 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.16s
1333251 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
1333251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1333251 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 113ns
1333251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1338464 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.21s
1338464 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1338464 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.9ns
1338464 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1340285 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1344060 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.59s