Standard output
744383 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
744383 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.3ns
744383 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
744524 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
744524 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
744524 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
744524 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
744993 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
746306 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
748479 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.09s
748479 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
748479 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.6ns
748495 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
751247 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s
751262 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
751262 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
751262 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.1ns
751278 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
753983 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s
753983 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
753983 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.13ms
753983 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
754922 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
756969 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s