Standard output
752114 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
752114 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 163ns
752114 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
752223 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
752223 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
752223 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
752223 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
752676 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
754146 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
756207 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.09s
756207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
756225 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.6ms
756225 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
759098 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s
759098 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
759098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
759098 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 106ns
759098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
761825 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s
761825 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
761825 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.5ns
761825 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
762794 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
764895 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s