Standard output
856783 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
856783 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.31ns
856784 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
856910 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
856911 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
856912 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
856912 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
857407 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
858792 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
861260 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.48s
861262 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
861262 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.71ns
861263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
864467 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s
864480 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
864481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
864481 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns
864482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
867611 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s
867612 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
867612 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns
867613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
868703 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
871136 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s