Standard output
826979 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
826979 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns
826979 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
827143 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
827143 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
827144 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
827144 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
827667 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
829068 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
831513 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.53s
831514 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
831515 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns
831515 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
834568 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s
834580 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
834581 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
834581 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns
834582 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
837561 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s
837562 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
837562 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.79ns
837563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
838616 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
840870 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s