Standard output
978142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
978142 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.5ns
978142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
978470 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
978470 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
978470 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
978470 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
979143 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
980721 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
983473 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.32s
983473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
983473 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 848.2ns
983473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
986975 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s
987006 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
987006 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
987006 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.2ns
987006 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
990525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s
990525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
990525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.9ns
990525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
991744 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
994231 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.71s