Standard output
1338291 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1338291 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.2ns
1338291 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1338526 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1338526 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1338526 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1338526 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1339385 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1341746 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1345562 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.27s
1345578 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1345578 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.1ns
1345578 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1350756 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.18s
1350788 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
1350788 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1350788 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.7ns
1350788 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1355884 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s
1355884 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1355884 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 429.9ns
1355884 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1357650 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1361496 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.61s