Standard output
1330228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1330228 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.3ns
1330228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1330478 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1330478 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1330478 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1330478 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1331306 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1333455 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1337922 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.69s
1337922 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1337922 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.17ms
1337938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1344736 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.81s
1344767 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
1344767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1344767 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.4ns
1344767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1349897 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.14s
1349897 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1349897 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.9ns
1349913 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1351684 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1355610 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.71s