Standard output
747133 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
747133 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.9ns
747133 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
747243 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
747243 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
747243 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
747243 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
747674 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
749029 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
751176 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.04s
751191 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
751191 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.01ms
751191 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
753979 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s
753994 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
753994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
753994 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.8ns
753994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
756801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s
756801 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
756801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.3ns
756817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
757766 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
759876 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s