source: CIVL/examples/arithmetic/quadratic2.cvl@ d48b845

#include <stdio.h>

$input int x, y, z, w;
$input int N, M, L, K;
$input int offset;

$assume 0< N && N <= 2;
$assume 0< M && M <= 2;
$assume 0< L && L <= 2;
$assume 0< K && K <= 2;
$assume 0 <= x && x < N;
$assume 0 <= y && y < M;
$assume 0 <= z && z < L;
$assume 0 <= w && w < K;
$assume 0 <= offset ;
$assume (offset + x*M*L*K + y*L*K + z*K + w) < M*N*L*K;

void main(){

  int realIndex, finalIndex, X, Y, Z, W;

  realIndex = x * M *  L * K + y * L * K + z * K + w;
  finalIndex = realIndex + offset;
  X = finalIndex / (M * L * K);
  finalIndex = finalIndex - X * M * L * K;
  Y = finalIndex / (L * K);
  finalIndex = finalIndex - Y * L * K;
  Z = finalIndex / K;
  W = finalIndex - Z * K;

  printf("X=%d, Y=%d, Z=%d, W=%d\n", X,Y,Z,W);
  $assert X < N;
  $assert Y < M;
  $assert Z < L;
  $assert W < K;
}