Standard output
875849 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
875849 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 148ns
875849 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
875974 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
875974 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
875974 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
875974 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
876513 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
878224 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
880659 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.8s
880659 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
880659 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.1ns
880659 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
883955 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s
883955 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
883971 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
883971 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.6ns
883971 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
887301 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s
887317 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
887317 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.1ns
887317 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
888454 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
892043 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.72s