Standard output
1452974 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
1452974 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.7ns
1452975 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1453202 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1453202 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1453203 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1453203 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1454274 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1456937 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1461869 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 8.89s
1461874 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
1461874 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.3ns
1461875 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1467442 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.57s
1467465 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
1467476 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
1467476 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns
1467476 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1472761 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.28s
1472762 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
1472762 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.6ns
1472763 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1474578 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1478624 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.86s