Standard output
805496 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
805497 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 660.8ns
805497 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
805616 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
805617 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
805617 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
805617 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
806209 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
807397 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
809897 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.4s
809899 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
809899 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.6ns
809900 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
813039 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s
813045 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
813046 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
813046 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns
813047 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
816108 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s
816109 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
816109 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns
816109 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
817106 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
819505 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s