Standard output
863996 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
863996 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.6ns
863996 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
864137 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
864137 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
864137 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
864137 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
864676 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
866568 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
870025 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.02s
870025 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
870025 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.67ms
870025 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
873374 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s
873389 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
873405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
873405 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.2ns
873405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
876680 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s
876680 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
876680 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.9ns
876680 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
877868 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
880241 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s