Standard output
909333 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
909334 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.2ns
909334 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
909486 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
909487 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
909487 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
909487 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
910140 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
911719 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
914449 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.12s
914452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
914452 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.1ns
914453 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
918036 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s
918050 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
918055 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
918055 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.7ns
918056 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
921613 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s
921614 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
921614 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.6ns
921615 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
922835 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
925461 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.85s