Standard output
834068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
834068 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.1ns
834068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
834197 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
834197 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
834198 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
834198 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
834719 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
836221 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
838529 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.46s
838531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
838531 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.11ns
838532 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
841729 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s
841748 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
841749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
841749 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.31ns
841750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
844946 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s
844947 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
844947 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns
844947 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
846034 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
848392 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s