Standard output
973408 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
973408 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.4ns
973408 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
973627 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
973627 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
973627 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
973627 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
974799 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
976315 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
979286 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.88s
979301 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
979301 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.1ns
979301 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
982991 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.7s
983022 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
983022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
983022 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 449.6ns
983038 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
986712 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.68s
986712 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
986712 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 154ns
986728 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
987915 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
990651 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.92s