Standard output
706583 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
706583 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.5ns
706583 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
706692 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
706692 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
706692 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
706692 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
707177 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
708255 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
710506 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.92s
710506 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
710506 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 924.5ns
710506 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
713211 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s
713227 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
713242 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
713242 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns
713242 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
715884 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s
715884 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
715884 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.3ns
715900 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
716823 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
718762 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s