Standard output
1343729 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
1343729 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.8ns
1343729 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1343923 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1343923 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1343924 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1343924 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
1344767 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
1346993 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1351048 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.32s
1351052 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
1351052 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.9ns
1351053 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1356390 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.34s
1356408 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
1356409 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
1356409 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns
1356409 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1361657 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.25s
1361659 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
1361659 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.5ns
1361660 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
1363515 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
1367504 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.84s