#include<string.h>
#include<stdio.h>

int main(){
  char a[5];

  memset(a, 0, 3);
  printf("%c, %c, %c, %c, %c\n", a[0], a[1],a[2],a[3],a[4]);
  //$assert $forall {i= 0 .. 2} a[i]==0;
  $assert a[0]==0;
}