Standard output
909469 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
909469 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.2ns
909469 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
909600 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
909600 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
909601 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
909601 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
910138 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
911588 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
914224 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.75s
914226 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
914226 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.7ns
914227 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
917743 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s
917770 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
917771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
917771 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.2ns
917772 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
921279 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s
921280 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
921280 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns
921281 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
922468 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
925087 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.81s