ContractLoadingTests

1079061    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java 
1079061    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.7ns 
1079061    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1079214    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1079214    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1079214    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1079214    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1079878    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
1081669    DEBUG Test worker     d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods. 
1084787    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.73s 
1084802    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java 
1084802    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.9ns 
1084802    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1089019    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.21s 
1089019    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 
1089019    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java 
1089019    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.5ns 
1089019    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1093235    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.21s 
1093235    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java 
1093235    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190ns 
1093235    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1094677    DEBUG Test worker     d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods. 
1097801    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.56s