Standard output
859723 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
859723 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.5ns
859723 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
859849 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
859849 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
859849 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
859849 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
860375 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
861823 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
864378 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.65s
864378 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
864378 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.2ns
864378 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
867686 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s
867701 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
867701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
867701 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.5ns
867701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
871025 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s
871025 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
871025 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.4ns
871041 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
872138 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
874415 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s