Standard output
652142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
652142 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.6ns
652143 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
652235 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
652235 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
652236 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
652236 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
652704 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
653809 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
655697 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s
655699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
655699 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.5ns
655700 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
658265 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s
658276 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
658278 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
658279 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.7ns
658279 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
660827 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s
660829 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
660829 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.7ns
660829 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
661728 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
663634 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s