Standard output
884120 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
884120 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 151ns
884136 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
884277 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
884277 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
884277 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
884277 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
884793 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
886385 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
889847 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.71s
889850 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
889850 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 557.6ns
889850 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
893342 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s
893357 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
893357 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
893357 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.3ns
893357 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
896653 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s
896653 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
896653 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.9ns
896653 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
898002 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
901170 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.52s