Standard output
781417 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
781417 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.6ns
781417 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
781558 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
781558 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
781558 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
781558 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
782120 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
783296 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
786764 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.35s
786782 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
786784 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.37ms
786787 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
789924 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s
789940 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
789955 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
789955 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.3ns
789955 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
792788 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s
792788 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
792788 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.7ns
792804 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
793789 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
795923 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s