Standard output
880554 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
880554 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 436.3ns
880555 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
880730 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
880738 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
880739 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
880739 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
881448 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
882980 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
885593 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.04s
885595 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
885595 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.4ns
885595 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
889057 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s
889080 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
889080 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
889081 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.7ns
889081 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
892513 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s
892514 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
892514 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns
892515 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
893640 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
896181 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.67s