Standard output
909127 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
909128 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 467.2ns
909128 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
909272 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
909272 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
909272 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
909272 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
909914 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
911610 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
914253 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.12s
914255 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
914255 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.3ns
914256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
917947 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.69s
917955 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
917956 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
917956 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns
917957 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
921563 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s
921565 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
921565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns
921565 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
922811 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
925390 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.82s