Standard output
944166 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
944166 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.6ns
944166 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
944325 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
944325 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
944325 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
944325 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
944972 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
946443 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
949459 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.29s
949474 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
949474 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 736.9ns
949474 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
953382 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.9s
953429 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
953429 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
953429 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.6ns
953445 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
957246 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.81s
957262 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
957262 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 406ns
957262 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
958515 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
961234 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.98s