Standard output
937827 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
937827 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142ns
937827 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
937999 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
937999 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
937999 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
937999 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
938609 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
940464 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
945361 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.54s
945380 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
945381 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.32ms
945385 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
948942 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s
948963 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
948963 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
948963 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns
948973 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
952340 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s
952340 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
952340 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.4ns
952355 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
953466 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
955926 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s