// 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 // 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:=*; // file pthreads.c line 7 // FROM Predicates: L0: b2_g_eq_0 := 1; // TO Predicates: b2_g_eq_0 // file line 12 // FROM Predicates: L1: skip; // no predicates changed // TO Predicates: // file 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: skip; // no predicates changed // TO Predicates: // file pthreads.c line 35 function main // FROM Predicates: L7: skip; // no predicates changed // TO Predicates: // file pthreads.c line 35 function main // FROM Predicates: L8: skip; // no predicates changed // TO Predicates: // file pthreads.c line 35 function main // FROM Predicates: L9: skip; // no predicates changed // TO Predicates: // file pthreads.c line 37 function main // FROM Predicates: L10: start_thread goto l1; // TO Predicates: // file pthreads.c line 37 function main // FROM Predicates: L11: skip; // no predicates changed // TO Predicates: // file pthreads.c line 37 function main // FROM Predicates: L12: assert(1); // TO Predicates: // file pthreads.c line 37 function main // FROM Predicates: L13: skip; // location only // TO Predicates: // file pthreads.c line 11 function t1 // FROM Predicates: L14: skip; // no predicates changed // TO Predicates: // file pthreads.c line 11 function t1 // FROM Predicates: L15: b0_a1_eq_10 := *; // TO Predicates: b0_a1_eq_10 // file pthreads.c line 11 function t1 // FROM Predicates: L16: skip; // no predicates changed // TO Predicates: // file pthreads.c line 13 function t1 // FROM Predicates: L17: skip; // no predicates changed // TO Predicates: // file pthreads.c line 14 function t1 // FROM Predicates: L18: b0_a1_eq_10 := *; // TO Predicates: b0_a1_eq_10 // file pthreads.c line 17 function t1 // FROM Predicates: 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: l1: L23: start_thread goto l2; // TO Predicates: // file pthreads.c line 38 function main // FROM Predicates: L24: skip; // no predicates changed // TO Predicates: // file pthreads.c line 38 function main // FROM Predicates: L25: assert(1); // TO Predicates: // file pthreads.c line 38 function main // FROM Predicates: L26: skip; // location only // TO Predicates: // file pthreads.c line 22 function t2 // FROM Predicates: L27: skip; // no predicates changed // TO Predicates: // file pthreads.c line 22 function t2 // FROM Predicates: L28: b1_a2_eq_20 := *; // TO Predicates: b1_a2_eq_20 // file pthreads.c line 22 function t2 // FROM Predicates: L29: skip; // no predicates changed // TO Predicates: // file pthreads.c line 24 function t2 // FROM Predicates: L30: skip; // no predicates changed // TO Predicates: // file pthreads.c line 25 function t2 // FROM Predicates: L31: b1_a2_eq_20 := *; // TO Predicates: b1_a2_eq_20 // file pthreads.c line 28 function t2 // FROM Predicates: 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