// The contrived program below checks if $x$ is divisible by N.
// Do note that in your cases N is a constant, which is at least 2.

// N is an experiment parameter; replace it with a concrete value.

divByN(x:int | divisible:bool) {
  // N is an experiment parameter
  assume x>1 ;
  var k:int {
    k := 1 ;
    divisible := false ;
    while k<=x && ~divisible do {
      //assert divisible
      //       =
      //       (exists m:: 0<m && m<k && m*N = x)  ;
      var i:int {
         i := 0 ;
         while i<N do { // deliberate bug ... should i<N. Change: removing the bug.
            i := i+1
         } ; // so, i = N
         divisible := i*k = x     // in other words, d := (N*k = x)
      } ;
      k := k+1
    }
  } ;
  assert divisible = (exists m:: 0<m && m<=x && m*N = x)
}