Standard output
859175 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
859175 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.8ns
859175 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
859363 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
859379 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
859379 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
859379 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
859863 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
861364 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
863912 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.73s
863912 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
863912 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 639.1ns
863912 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
867148 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s
867163 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
867163 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
867163 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.9ns
867179 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
870462 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s
870462 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
870462 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 174ns
870462 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
871619 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
874043 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s