Standard output
926591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
926591 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.3ns
926591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
926747 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
926747 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
926747 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
926747 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
927403 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
929060 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
932062 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.48s
932062 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
932062 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.7ns
932062 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
935926 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.85s
935942 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
935942 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
935942 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.8ns
935942 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
939681 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s
939681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
939681 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.1ns
939681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
940949 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
943778 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s