Standard output
927623 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
927623 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.5ns
927639 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
927795 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
927795 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
927795 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
927795 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
928407 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
929832 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
932785 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.16s
932803 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
932805 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 967.4ns
932807 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
936416 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s
936526 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
936526 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
936526 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.6ns
936526 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
941290 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.76s
941290 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
941290 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 466.1ns
941290 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
942483 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
945728 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.43s