Standard output
747774 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
747774 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.4ns
747774 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
747992 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
747992 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
747992 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
747992 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
748664 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
749946 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
752103 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.34s
752103 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
752119 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 859ns
752119 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
754902 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
754918 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
754918 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
754918 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.5ns
754933 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
757669 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s
757669 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
757669 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.5ns
757669 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
758638 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
760671 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s