Standard output
1227392 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1227392 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.6ns
1227392 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1227595 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1227595 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1227595 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1227595 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1228477 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1230568 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1234137 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.74s
1234137 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1234137 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 472.9ns
1234152 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1238760 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.61s
1238775 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
1238775 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1238775 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.5ns
1238775 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1243436 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.66s
1243436 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1243436 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.9ns
1243436 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1245058 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1248567 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.12s