Standard output
1303677 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1303677 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.7ns
1303677 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1303865 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1303865 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1303865 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1303865 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1304730 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1307076 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1310883 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.21s
1310883 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1310899 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 456ns
1310899 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1316025 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.12s
1316025 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
1316025 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1316025 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.2ns
1316025 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1321029 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5s
1321029 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1321029 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.6ns
1321029 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1322711 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1326535 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.49s