Standard output
1274595 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
1274595 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.7ns
1274595 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1274815 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1274815 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1274816 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1274816 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1275560 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1277702 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1281498 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.9s
1281501 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
1281501 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.8ns
1281502 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1286518 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.02s
1286527 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
1286528 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
1286528 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns
1286528 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1291480 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s
1291481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
1291481 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns
1291481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1293131 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1296849 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.37s