Standard output
911126 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java
911126 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.3ns
911126 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
911283 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
911283 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
911283 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
911283 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
912017 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
913518 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
916144 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.02s
916160 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java
916160 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.1ns
916160 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
919631 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s
919662 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
919662 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java
919662 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.7ns
919662 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
923165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s
923165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java
923165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.7ns
923165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
924384 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
927011 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.84s