Standard output
664121 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
664122 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns
664122 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
664216 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
664216 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
664216 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
664216 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
664612 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
665701 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
667695 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s
667696 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
667697 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.7ns
667697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
670230 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s
670240 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
670242 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
670242 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.1ns
670243 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
672779 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s
672780 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
672780 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns
672781 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
673655 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
675548 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s