Standard output
819847 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
819847 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns
819848 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
819963 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
819963 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
819963 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
819963 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
820516 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
821871 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
824178 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.33s
824181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
824181 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.31ns
824182 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
827351 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s
827364 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
827367 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
827367 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.41ns
827368 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
830435 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s
830436 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
830436 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns
830437 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
831498 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
833816 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s