Standard output
864687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
864688 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.3ns
864688 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
864820 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
864820 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
864821 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
864821 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
865366 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
866877 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
869278 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.59s
869281 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
869282 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 417.2ns
869282 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
872586 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s
872595 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
872599 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
872599 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.7ns
872600 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
875833 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s
875835 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
875835 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.6ns
875836 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
876941 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
879381 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s