Standard output
823940 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
823940 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 135ns
823941 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
824097 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
824097 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
824098 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
824098 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
824586 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
825967 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
828303 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.36s
828305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
828305 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns
828305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
831340 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s
831352 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
831353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
831353 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns
831354 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
834360 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s
834361 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
834361 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns
834362 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
835465 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
837798 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s