Standard output
1304457 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
1304457 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.4ns
1304458 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1304700 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1304700 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1304701 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1304701 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1305431 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1307630 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1311674 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.22s
1311677 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
1311677 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.8ns
1311678 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1316958 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.28s
1316968 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
1316971 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
1316971 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 96ns
1316971 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1322092 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.12s
1322093 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
1322093 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns
1322094 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1323823 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1327721 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.63s