Standard output
894075 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
894075 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.3ns
894075 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
894278 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
894278 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
894278 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
894278 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
895295 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
897127 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
900427 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.36s
900458 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
900458 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 597.9ns
900458 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
903919 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s
903951 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
903951 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
903951 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.4ns
903951 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
907397 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s
907397 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
907397 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.4ns
907413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
908556 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
911168 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.76s