Standard output
1106212 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
1106212 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.21ns
1106212 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1106402 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1106402 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1106402 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1106402 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1107108 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1108921 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1112184 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.97s
1112187 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
1112187 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 652.44ns
1112188 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1116583 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.4s
1116602 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
1116603 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
1116603 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.41ns
1116604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1121009 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.4s
1121011 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
1121011 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.52ns
1121012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1122532 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1125797 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.79s