Standard output
1139740 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
1139740 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.7ns
1139741 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1139897 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1139897 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1139898 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1139898 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1140559 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1142528 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1145817 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.08s
1145819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
1145819 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 146ns
1145820 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1150271 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.45s
1150294 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
1150298 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
1150298 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.4ns
1150299 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1154709 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.41s
1154710 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
1154710 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.4ns
1154711 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1156229 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1159506 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.8s