Standard output
1275226 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1275226 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 199ns
1275226 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1275462 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1275462 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1275462 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1275462 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1276212 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1278379 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1282112 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.88s
1282112 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1282112 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.1ns
1282112 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1287101 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5s
1287117 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
1287117 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1287117 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.5ns
1287117 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1292001 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s
1292017 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1292017 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.4ns
1292017 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1293700 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1297568 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.55s