Standard output
928115 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
928115 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.6ns
928130 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
928255 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
928255 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
928255 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
928255 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
928990 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
930429 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
933071 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.94s
933076 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
933076 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.02ms
933076 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
936588 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s
936619 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
936619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
936619 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.2ns
936619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
939979 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s
939995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
939995 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230ns
939995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
941183 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
943606 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.62s