Standard output
1399697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1399697 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.4ns
1399697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1400012 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1400012 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1400012 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1400012 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1400891 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1403045 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1408617 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 8.91s
1408635 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1408635 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.21ms
1408635 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1414235 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.6s
1414267 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
1414267 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1414267 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.7ns
1414267 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1419565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.3s
1419565 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1419565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 204ns
1419565 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1421425 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1425468 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.9s