Standard output
927067 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
927067 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.8ns
927067 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
927229 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
927229 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
927230 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
927230 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
927883 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
929545 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
932211 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.14s
932213 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
932213 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.2ns
932214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
935807 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s
935823 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
935827 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
935828 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.5ns
935829 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
939341 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s
939343 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
939343 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.9ns
939344 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
940608 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
943201 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s