Standard output
768139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
768139 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.5ns
768139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
768264 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
768264 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
768264 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
768264 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
768768 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
769959 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
772464 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.32s
772464 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
772464 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 880ns
772464 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
775260 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s
775276 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
775276 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
775276 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.3ns
775276 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
778065 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s
778065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
778065 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 163ns
778065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
779034 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
781731 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.67s