Standard output
810960 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
810961 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.1ns
810961 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
811081 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
811081 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
811082 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
811082 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
811603 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
812822 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
815673 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.71s
815676 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
815677 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 368.6ns
815677 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
818994 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s
819007 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
819009 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
819009 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.9ns
819010 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
822079 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s
822080 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
822080 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns
822081 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
823100 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
825356 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s