Standard output
966043 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
966043 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.2ns
966044 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
966205 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
966206 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
966206 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
966206 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
966814 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
968532 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
971274 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.23s
971276 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
971276 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.5ns
971277 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
975033 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.76s
975054 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
975059 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
975059 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.7ns
975061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
978814 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.75s
978816 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
978816 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns
978817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
980087 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
982882 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.06s