Standard output
1245897 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
1245897 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224ns
1245898 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1246104 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1246104 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1246104 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1246104 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1246864 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1248993 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1252707 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.81s
1252709 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
1252710 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.3ns
1252710 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1257665 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s
1257671 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
1257672 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
1257673 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns
1257673 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1262431 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.76s
1262432 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
1262432 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns
1262433 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1264024 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1267466 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s