Standard output
699200 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
699200 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns
699201 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
699317 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
699318 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
699318 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
699318 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
699776 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
701063 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
703046 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.85s
703049 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
703049 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 377ns
703050 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
705689 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s
705699 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
705703 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
705703 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.4ns
705704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
708370 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s
708371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
708371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns
708372 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
709293 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
711295 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s