Example how to generate a Boolean Program

#define NULL 0

typedef int pthread_t;

int pthread_create(pthread_t *, void *, void *, void *);

int g;

void *t1(void *arg) {

	int a1, *aptr1;

	aptr1 = (int *) arg;

	a1 = *aptr1;

	// this should pass
	assert(a1 == 10);
}

void *t2(void *arg) {
	int a2, *aptr2;

	aptr2 = (int *) arg;
	a2 = *aptr2;

	// this should pass
	assert(a2 == 20);
}

int main() {

	pthread_t id1, id2;

	int arg1 = 10, arg2 = 20;

	pthread_create(&id1, NULL, t1, &arg1);
	pthread_create(&id2, NULL, t2, &arg2);

	assert(g == 0);
}

// automatically generated by CPROVER/SATABS

// global variables of the abstract program

decl b0_a1_eq_10;    // a1 == 10

decl b1_a2_eq_20;    // a2 == 20
decl b2_g_eq_0;      // g == 0
decl b3_arg1_eq_10;  // arg1 == 10

decl b4_arg2_eq_20;  // arg2 == 20

// main
void main() begin

      // the local variables

      // initialization of the global variables


      b0_a1_eq_10:=*; 
      b1_a2_eq_20:=*; 
      b2_g_eq_0:=*; 
      b3_arg1_eq_10:=*; 
      b4_arg2_eq_20:=*; 

  L0: b2_g_eq_0 := 1;

  L6: b3_arg1_eq_10 := *;
  L7: b3_arg1_eq_10 := 1;

  L8: b4_arg2_eq_20 := *;
  L9: b4_arg2_eq_20 := 1;

 L10: start_thread goto l1;
 L11: skip; // no predicates changed

 L12: assert(1);
 L15: b0_a1_eq_10 := *;

 L18: b0_a1_eq_10 := b3_arg1_eq_10;
 L19: assert(b0_a1_eq_10);

 L22: end_thread;
  l1:
 L23: start_thread goto l2;

 L25: assert(1);
 L28: b1_a2_eq_20 := *;

 L31: b1_a2_eq_20 := b4_arg2_eq_20;
 L32: assert(b1_a2_eq_20);

 L35: end_thread;
  l2:
 L36: assert(b2_g_eq_0);

end