Standard output
1266447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1266447 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.7ns
1266447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1266650 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1266650 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1266650 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1266650 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1267401 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1269739 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1275516 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 9.07s
1275532 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1275532 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 620.7ns
1275537 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1280543 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s
1280559 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
1280559 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1280559 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.2ns
1280559 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1285418 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.87s
1285434 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1285434 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.6ns
1285434 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1287122 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1290759 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.32s