Standard output
778592 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
778592 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.1ns
778593 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
778712 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
778713 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
778713 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
778713 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
779152 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
780504 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
782839 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s
782842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
782842 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.91ns
782843 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
785864 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s
785876 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
785878 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
785878 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.4ns
785879 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
788820 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s
788821 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
788821 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns
788822 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
789870 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
792110 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s