Standard output
1310339 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1310339 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.6ns
1310355 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1310526 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1310526 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1310526 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1310526 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1311311 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1313480 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1317391 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.05s
1317407 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1317407 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.4ns
1317407 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1322627 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.23s
1322643 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
1322643 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1322643 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 114ns
1322643 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1327829 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.17s
1327829 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1327829 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.1ns
1327829 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1329596 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1333425 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.6s