Standard output
1127120 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1127120 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.9ns
1127120 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1127292 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1127292 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1127292 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1127292 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1127964 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1129997 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1133342 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.22s
1133358 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1133358 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.9ns
1133358 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1138065 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.7s
1138081 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
1138081 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1138081 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.2ns
1138081 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1142677 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.59s
1142677 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1142677 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.1ns
1142677 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1144256 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1147509 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.83s