ContractLoadingTests

893210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java 
893210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.1ns 
893211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
893350     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
893350     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
893351     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
893351     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
893933     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
895560     DEBUG Test worker     d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods. 
898109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.9s 
898111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java 
898111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.7ns 
898112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
901511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
901537     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 
901538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java 
901538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
901539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
904921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
904924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java 
904924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.8ns 
904925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
906079     DEBUG Test worker     d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods. 
908645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.72s