Standard output
1078688 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
1078688 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.1ns
1078688 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1078845 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1078860 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1078861 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1078861 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1079517 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1081393 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1084428 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.73s
1084428 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
1084428 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.5ns
1084428 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1088555 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.12s
1088571 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
1088571 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
1088571 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.9ns
1088571 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1092667 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.09s
1092667 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
1092667 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.5ns
1092667 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1094059 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1097123 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.46s