Standard output
749554 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
749554 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 215ns
749554 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
749664 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
749664 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
749664 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
749664 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
750225 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
751468 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
753615 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.05s
753615 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
753615 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.21ms
753615 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
756549 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s
756565 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
756565 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
756565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.4ns
756580 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
759473 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s
759473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
759473 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.1ns
759473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
760460 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
762608 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s