Standard output
1184952 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
1184953 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.3ns
1184953 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1185136 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1185136 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1185137 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1185137 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1185951 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1187915 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1191335 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.38s
1191337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
1191338 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.3ns
1191338 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1196112 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.77s
1196121 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
1196125 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
1196125 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.4ns
1196126 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1200834 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.71s
1200836 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
1200837 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 326ns
1200837 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1202455 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1205994 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.16s