Standard output
1180670 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
1180671 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 457.1ns
1180672 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1180895 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1180895 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1180895 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1180895 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1181701 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1183845 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1187486 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.81s
1187489 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
1187489 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.8ns
1187489 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1192411 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.92s
1192424 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
1192425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
1192425 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns
1192425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1197241 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.82s
1197243 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
1197244 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 401.9ns
1197245 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1198852 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1202316 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.07s