Standard output
899427 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
899427 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns
899428 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
899563 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
899563 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
899565 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
899565 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
900216 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
901689 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
904362 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.93s
904364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
904364 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.1ns
904365 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
907852 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s
907859 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
907860 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
907860 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns
907861 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
911290 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s
911292 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
911292 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns
911292 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
912473 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
915096 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.8s