Standard output
1253863 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
1253864 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 628.4ns
1253864 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1254121 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1254122 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1254123 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1254123 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1254915 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1257148 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1260777 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.91s
1260781 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
1260781 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.9ns
1260782 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1265638 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.86s
1265645 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
1265646 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
1265646 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns
1265646 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1270424 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.78s
1270425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
1270425 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns
1270426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1272081 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1275677 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.25s