Standard output
877080 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
877080 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 587.9ns
877080 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
877205 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
877205 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
877205 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
877205 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
877752 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
879112 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
881749 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.67s
881749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
881749 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.39ms
881749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
885254 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s
885348 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
885348 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
885348 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.1ns
885348 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
889296 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.94s
889296 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
889296 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.7ns
889296 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
890445 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
892925 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s