Standard output
1093429 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1093429 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.8ns
1093445 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1093586 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1093586 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1093586 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1093586 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1094180 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1095989 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1099343 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.9s
1099343 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1099343 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.8ns
1099343 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1103611 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.26s
1103611 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
1103611 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1103611 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.3ns
1103611 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1107838 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s
1107838 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1107838 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.5ns
1107853 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1109313 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1112525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.68s