Standard output
1437444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1437444 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.7ns
1437444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1437648 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1437648 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1437648 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1437648 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1438441 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1440654 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1445893 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 8.45s
1445912 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1445912 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.22ms
1445912 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1451565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.65s
1451581 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
1451581 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1451581 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.7ns
1451581 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1457158 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.57s
1457158 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1457158 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.5ns
1457158 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1459071 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1463918 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.76s