Standard output
909898 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
909898 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.5ns
909914 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
910055 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
910055 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
910055 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
910055 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
910665 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
912196 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
914917 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s
914917 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
914917 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.2ns
914932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
918357 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s
918388 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
918388 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
918388 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.8ns
918388 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
921749 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s
921749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
921749 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.4ns
921749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
922938 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
925501 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.74s