# language: C
c

# Context
#{M | 3<=M}
2 3
#   M   1
1   1  -3
1   0   1
0

4 # Number of statements

1
#{i,j,k | i=1; j=1; 2<=k<=M; 3<=M}
6 6
#   i   j   k    M    1
0   1   0   0    0   -1
0   0   1   0    0   -1
1   0   0   0    1   -3
1   0   0   -1   1   0
1   0   0   1    0   -2
1   0   0   0    0   1
0 0 0

1
#{i,j,k | 2<=i<=k-1; j=1; k<=M}
5 6
#   i    j   k    M    1
0   0    1   0    0   -1
1   -1   0   1    0   -1
1   1    0   0    0   -2
1   0    0   -1   1   0
1   0    0   0    0   1
0 0 0

1
#{i,j | i=1; j=0; 3<=M}
4 5
#   i   j   M    1
0   1   0   0   -1
0   0   1   0   0
1   0   0   1   -3
1   0   0   0   1
0 0 0

1
#{i,j | 2<=i<=M; j=0; 3<=M}
4 5
#   i    j   M    1
0   0    1   0   0
1   1    0   0   -2
1   0    0   1   -3
1   -1   0   1   0
0 0 0
0

0 # Scattering functions