Standard output
803213 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
803213 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 106ns
803214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
803330 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
803330 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
803331 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
803331 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
803842 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
805196 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
807630 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.42s
807632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
807633 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.9ns
807633 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
810826 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s
810838 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
810842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
810842 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.9ns
810843 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
814023 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s
814025 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
814025 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.2ns
814027 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
815121 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
817475 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s