Standard output
1014875 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1014875 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.4ns
1014875 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1015031 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1015031 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1015031 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1015031 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1015547 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1017257 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1020334 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.46s
1020334 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1020334 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.2ns
1020350 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1024267 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.93s
1024283 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
1024283 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1024283 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns
1024283 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1028165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s
1028165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1028165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns
1028165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1029487 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1032394 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s