Standard output
744644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
744644 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 157ns
744644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
744753 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
744753 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
744753 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
744753 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
745175 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
746410 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
748537 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s
748537 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
748537 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.7ns
748537 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
751226 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s
751242 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
751242 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
751242 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.1ns
751242 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
753961 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s
753961 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
753977 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.6ns
753977 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
754915 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
756933 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s