Standard output
940380 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
940380 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.3ns
940380 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
940536 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
940536 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
940536 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
940536 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
941115 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
942428 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
945431 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.06s
945447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
945447 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 696.4ns
945447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
948824 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s
948855 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
948855 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
948855 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.8ns
948871 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
952186 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s
952202 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
952202 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.7ns
952202 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
953281 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
955594 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s