Standard output
826586 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
826586 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.4ns
826586 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
826742 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
826742 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
826742 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
826742 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
827368 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
828931 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
831776 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.18s
831776 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
831776 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.2ns
831776 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
835154 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s
835185 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
835185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
835185 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 111ns
835185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
838609 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s
838609 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
838609 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.6ns
838609 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
839813 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
842440 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.83s