// 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

  // 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:=*; 

    // file pthreads.c line 7
    // FROM Predicates:
  L0: b2_g_eq_0 := 1;
    // TO Predicates: b2_g_eq_0

    // file <built-in> line 12
    // FROM Predicates:
  L1: skip; // no predicates changed
    // TO Predicates:

    // file <built-in> line 13
    // FROM Predicates:
  L2: skip; // no predicates changed
    // TO Predicates:

    // FROM Predicates:
  L3: skip; // location only
    // TO Predicates:

    // file pthreads.c line 33 function main
    // FROM Predicates:
  L4: skip; // no predicates changed
    // TO Predicates:

    // file pthreads.c line 33 function main
    // FROM Predicates:
  L5: skip; // no predicates changed
    // TO Predicates:

    // file pthreads.c line 35 function main
    // FROM Predicates:
  L6: b3_arg1_eq_10 := *;
    // TO Predicates: b3_arg1_eq_10

    // file pthreads.c line 35 function main
    // FROM Predicates:
  L7: b3_arg1_eq_10 := 1;
    // TO Predicates: b3_arg1_eq_10

    // file pthreads.c line 35 function main
    // FROM Predicates: b3_arg1_eq_10
  L8: b4_arg2_eq_20 := *;
    // TO Predicates: b3_arg1_eq_10 b4_arg2_eq_20

    // file pthreads.c line 35 function main
    // FROM Predicates: b3_arg1_eq_10
  L9: b4_arg2_eq_20 := 1;
    // TO Predicates: b3_arg1_eq_10 b4_arg2_eq_20

    // file pthreads.c line 37 function main
    // FROM Predicates: b3_arg1_eq_10 b4_arg2_eq_20
 L10: start_thread goto l1;
    // TO Predicates: b3_arg1_eq_10 b4_arg2_eq_20

    // file pthreads.c line 37 function main
    // FROM Predicates: b3_arg1_eq_10
 L11: skip; // no predicates changed
    // TO Predicates: b3_arg1_eq_10

    // file pthreads.c line 37 function main
    // FROM Predicates: b3_arg1_eq_10
 L12: assert(1);
    // TO Predicates: b3_arg1_eq_10

    // file pthreads.c line 37 function main
    // FROM Predicates: b3_arg1_eq_10
 L13: skip; // location only
    // TO Predicates: b3_arg1_eq_10

    // file pthreads.c line 11 function t1
    // FROM Predicates: b3_arg1_eq_10
 L14: skip; // no predicates changed
    // TO Predicates: b3_arg1_eq_10

    // file pthreads.c line 11 function t1
    // FROM Predicates: b3_arg1_eq_10
 L15: b0_a1_eq_10 := *;
    // TO Predicates: b0_a1_eq_10 b3_arg1_eq_10

    // file pthreads.c line 11 function t1
    // FROM Predicates: b3_arg1_eq_10
 L16: skip; // no predicates changed
    // TO Predicates: b3_arg1_eq_10

    // file pthreads.c line 13 function t1
    // FROM Predicates: b3_arg1_eq_10
 L17: skip; // no predicates changed
    // TO Predicates: b3_arg1_eq_10

    // file pthreads.c line 14 function t1
    // FROM Predicates: b3_arg1_eq_10
 L18: b0_a1_eq_10 := b3_arg1_eq_10;
    // TO Predicates: b0_a1_eq_10

    // file pthreads.c line 17 function t1
    // FROM Predicates: b0_a1_eq_10
 L19: assert(b0_a1_eq_10);
    // TO Predicates:

    // file pthreads.c line 18 function t1
    // FROM Predicates:
 L20: skip; // no predicates changed
    // TO Predicates:

    // file pthreads.c line 18 function t1
    // FROM Predicates:
 L21: skip; // location only
    // TO Predicates:

    // FROM Predicates:
 L22: end_thread;
    // TO Predicates:

    // file pthreads.c line 38 function main
    // FROM Predicates: b4_arg2_eq_20
  l1:
 L23: start_thread goto l2;
    // TO Predicates: b4_arg2_eq_20

    // file pthreads.c line 38 function main
    // FROM Predicates: b4_arg2_eq_20
 L24: skip; // no predicates changed
    // TO Predicates: b4_arg2_eq_20

    // file pthreads.c line 38 function main
    // FROM Predicates: b4_arg2_eq_20
 L25: assert(1);
    // TO Predicates: b4_arg2_eq_20

    // file pthreads.c line 38 function main
    // FROM Predicates: b4_arg2_eq_20
 L26: skip; // location only
    // TO Predicates: b4_arg2_eq_20

    // file pthreads.c line 22 function t2
    // FROM Predicates: b4_arg2_eq_20
 L27: skip; // no predicates changed
    // TO Predicates: b4_arg2_eq_20

    // file pthreads.c line 22 function t2
    // FROM Predicates: b4_arg2_eq_20
 L28: b1_a2_eq_20 := *;
    // TO Predicates: b1_a2_eq_20 b4_arg2_eq_20

    // file pthreads.c line 22 function t2
    // FROM Predicates: b4_arg2_eq_20
 L29: skip; // no predicates changed
    // TO Predicates: b4_arg2_eq_20

    // file pthreads.c line 24 function t2
    // FROM Predicates: b4_arg2_eq_20
 L30: skip; // no predicates changed
    // TO Predicates: b4_arg2_eq_20

    // file pthreads.c line 25 function t2
    // FROM Predicates: b4_arg2_eq_20
 L31: b1_a2_eq_20 := b4_arg2_eq_20;
    // TO Predicates: b1_a2_eq_20

    // file pthreads.c line 28 function t2
    // FROM Predicates: b1_a2_eq_20
 L32: assert(b1_a2_eq_20);
    // TO Predicates:

    // file pthreads.c line 29 function t2
    // FROM Predicates:
 L33: skip; // no predicates changed
    // TO Predicates:

    // file pthreads.c line 29 function t2
    // FROM Predicates:
 L34: skip; // location only
    // TO Predicates:

    // FROM Predicates:
 L35: end_thread;
    // TO Predicates:

    // file pthreads.c line 40 function main
    // FROM Predicates:
  l2:
 L36: assert(b2_g_eq_0);
    // TO Predicates:

    // file pthreads.c line 41 function main
    // FROM Predicates:
 L37: skip; // no predicates changed
    // TO Predicates:

    // file pthreads.c line 41 function main
    // FROM Predicates:
 L38: skip; // location only
    // TO Predicates:

    // FROM Predicates:
 L39: skip;
    // TO Predicates:

end