Standard output
852862 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
852863 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.5ns
852863 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
852998 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
852998 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
852999 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
852999 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
853525 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
855019 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
857416 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.55s
857418 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
857419 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.6ns
857419 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
860622 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s
860646 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
860647 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
860647 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns
860647 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
863923 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s
863926 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
863926 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.4ns
863926 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
865000 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
867366 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s