Standard output
1136967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1136967 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.1ns
1136967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1137139 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1137139 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1137139 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1137139 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1137936 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1139892 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1143237 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.28s
1143253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1143253 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 577.8ns
1143253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1147881 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.63s
1147897 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
1147897 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1147897 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.3ns
1147897 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1152526 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.62s
1152526 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1152526 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.8ns
1152526 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1154089 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1157466 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.94s