Standard output
985753 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
985753 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.8ns
985769 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
985925 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
985925 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
985925 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
985925 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
986615 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
988319 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
991305 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.54s
991305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
991305 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 990.1ns
991305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
994996 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.68s
995012 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
995027 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
995027 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.2ns
995027 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
998655 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.63s
998655 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
998655 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.2ns
998655 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
999953 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1002595 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.94s