Standard output
906499 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
906499 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.4ns
906514 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
906654 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
906654 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
906654 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
906654 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
907191 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
908498 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
911076 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.57s
911076 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
911076 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 830.5ns
911092 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
914442 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s
914504 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
914504 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
914504 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.1ns
914504 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
918744 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.23s
918744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
918744 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.4ns
918744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
919849 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
922213 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s