Standard output
734001 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
734001 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.8ns
734001 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
734278 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
734278 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
734278 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
734278 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
734907 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
736165 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
738494 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.49s
738510 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
738510 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 845.9ns
738510 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
741207 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s
741222 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
741222 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
741222 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.2ns
741238 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
743908 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s
743908 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
743908 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.5ns
743908 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
744849 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
747564 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s