Standard output
1104260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
1104260 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.31ns
1104260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1104417 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1104417 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1104417 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1104417 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1105008 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1106931 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1110206 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.95s
1110208 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
1110209 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.41ns
1110209 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1114533 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.32s
1114543 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
1114547 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
1114547 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.92ns
1114548 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1118829 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s
1118831 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
1118831 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 412.12ns
1118832 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1120326 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1123599 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.77s