Standard output
795026 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
795026 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.4ns
795026 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
795151 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
795151 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
795167 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
795167 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
795699 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
797215 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
799888 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.86s
799888 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
799888 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.11ms
799888 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
803157 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s
803188 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
803188 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
803188 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.5ns
803188 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
806488 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s
806488 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
806488 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.6ns
806488 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
807613 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
810052 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s