Standard output
772747 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
772763 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.2ns
772763 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
772889 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
772889 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
772889 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
772889 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
773318 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
774828 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
776979 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s
776979 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
776979 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.39ms
776979 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
780189 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s
780298 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
780298 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
780298 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.3ns
780298 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
783936 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s
783952 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
783952 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.3ns
783953 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
784968 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
787176 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s