Standard output
924909 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
924909 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 147ns
924909 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
925066 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
925066 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
925066 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
925066 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
925644 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
927302 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
929756 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.85s
929756 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
929756 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.29ms
929771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
933071 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s
933086 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
933086 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
933086 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns
933086 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
936525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s
936525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
936525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.3ns
936525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
937761 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
940278 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.75s