Standard output
947353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
947353 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.8ns
947353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
947509 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
947509 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
947509 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
947509 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
948163 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
949618 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
952642 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.28s
952643 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
952643 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 698.9ns
952643 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
956210 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s
956233 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
956233 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
956233 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.8ns
956233 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
959783 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s
959783 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
959783 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 413.5ns
959798 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
960988 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
964286 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.5s