Standard output
878607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
878607 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.2ns
878608 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
878819 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
878820 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
878820 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
878820 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
879406 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
881022 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
883617 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s
883620 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
883620 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.3ns
883621 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
887048 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s
887070 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
887071 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
887071 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns
887071 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
890473 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s
890474 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
890474 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.7ns
890475 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
891636 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
894128 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s