Standard output
664470 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
664470 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.8ns
664470 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
664584 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
664584 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
664584 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
664584 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
665147 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
666296 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
668484 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.01s
668484 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
668484 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.5ns
668484 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
671242 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s
671258 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
671258 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
671258 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.4ns
671258 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
673971 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s
673971 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
673971 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.2ns
673971 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
674908 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
676972 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s