#include<stdio.h>
#include <klee/klee.h>

int l[2] = {0,0}, r[2] = {0,0};
// int l[2] , r[2];
int main() {
  // l[0] = l[1] = r[0] = r[1] = 0;
  int c1;
  klee_make_symbolic(&c1, sizeof(int), "c1");
  if(c1 == 0) {
    if (!r[1])
    {
      l[0] = 1; 
    }
  }
  else if(c1 == 1) {
    if (!l[1])
    {
      r[0] = 1;
    }
  }
  else if(c1 == 2) {
    if (l[0] == 1 && r[0] == 1)
    { 
      klee_assert(0);
    }
  }

  int c2;
  klee_make_symbolic(&c2, sizeof(int), "c2");
  if(c2 == 0) {
    if (!r[1])
    {
      l[0] = 1; 
    }
  }
  else if(c2 == 1) {
    if (!l[1])
    {
      r[0] = 1;
    }
  }
  else if(c2 == 2) {
    if (l[0] == 1 && r[0] == 1)
    {
      klee_assert(0);
    }
  }

  int c3;
  klee_make_symbolic(&c3, sizeof(int), "c3");
  if(c3 == 0) {
    if (!r[1])
    {
      l[0] = 1; 
    }
  }
  else if(c3 == 1) {
    if (!l[1])
    {
      r[0] = 1;
    }
  }
  else if(c3 == 2) {
    if (l[0] == 1 && r[0] == 1)
    { 
      klee_assert(0);
    }
  }
  return 0;
}