/*
 *  generated by CSeq [ 0000 / 0000 ]
 * 
 *                      2C9F merger-0.0-2015.07.09
 *                      FB59 parser-0.0-2015.06.26
 *                      AB0B module-0.0-2015.07.16 ]
 *
 *  2015-07-22 16:55:29
 *
 *  params:
 *    -i svcomp2015_unsafe/pthread-ext/25_stack_longer_false-unreach-call.c, --time 750, --unwind 2, --rounds 1, 
 *
 *  modules:
 *    4062 workarounds-0.0 ()
 *    5E66 functiontracker-0.0 ()
 *    AE03 preinstrumenter-0.0 (error-label)
 *    8CEB constants-0.0 ()
 *    6EDD spinlock-0.0 ()
 *    9C8E switchconverter-0.0 ()
 *    6A40 dowhileconverter-0.0 ()
 *    B23B conditionextractor-0.0 ()
 *    BB48 varnames-0.0 ()
 *    698C inliner-0.0 ()
 *    1629 unroller-0.0 (unwind)
 *    8667 duplicator-0.0 ()
 *    72E0 condwaitconverter-0.0 ()
 *    454D lazyseq-0.0 (rounds schedule threads deadlock)
 *    2B01 instrumenter-0.0 (backend bitwidth header)
 *    A4A2 feeder-0.0 (backend time llvm)
 *    07D4 cex-0.0 (backend linemap cex exitcode threadnamesmap threadindexes threadindextoname varnamesmap coordstofunctions)
 *
 */
#include <stdio.h>
#include <stdlib.h>
#define THREADS 2
#define ROUNDS 1
#define STOP_VOID(A) return;
#define STOP_NONVOID(A) return 0;
#define IF(T,A,B) if ((__cs_pc[T] > A) | (A >= __cs_pc_cs[T])) goto B;
#ifndef NULL
#define NULL 0
#endif
                                        unsigned __CPROVER_bitvector[1] __cs_active_thread[THREADS + 1] = {1};
                                        unsigned __CPROVER_bitvector[6] __cs_pc[THREADS + 1];
                                        unsigned __CPROVER_bitvector[7] __cs_pc_cs[THREADS + 1];
                                        unsigned int __cs_thread_index;
                                        unsigned __CPROVER_bitvector[6] __cs_thread_lines[] = {3, 32, 32};
                                        void *__cs_safe_malloc(int __cs_size)
                                        {
                                        void *__cs_ptr = malloc(__cs_size);
                                        __CPROVER_assume(__cs_ptr);
                                        		return __cs_ptr;
                                        }
                                        void __cs_init_scalar(void *__cs_var, int __cs_size)
                                        {
                                        if (__cs_size == (sizeof(int)))
                                        *((int *) __cs_var) = nondet_int();
                                        		else
                                        		{
                                        char *__cs_ptr = (char *) __cs_var;
                                        int __cs_j;
                                        		}
                                        }
                                        void __CSEQ_message(char *__cs_message)
                                        {
                                        		;
                                        }
                                        typedef int __cs_t;
                                        void *__cs_threadargs[THREADS + 1];
                                        int __cs_create(__cs_t *__cs_new_thread_id, void *__cs_attr, void *(*__cs_t)(void *), void *__cs_arg, int __cs_threadID)
                                        {
                                        if (__cs_threadID > THREADS)
                                        				return 0;
                                        *__cs_new_thread_id = __cs_threadID;
                                        __cs_active_thread[__cs_threadID] = 1;
                                        __cs_threadargs[__cs_threadID] = __cs_arg;
                                        __CSEQ_message("thread spawned");
                                        return 0;
                                        }
                                        int __cs_join(__cs_t __cs_id, void **__cs_value_ptr)
                                        {
                                        __CPROVER_assume(__cs_pc[__cs_id] == __cs_thread_lines[__cs_id]);
                                        return 0;
                                        }
                                        int __cs_exit(void *__cs_value_ptr)
                                        {
                                        		return 0;
                                        }
                                        typedef int __cs_mutex_t;
                                        int __cs_mutex_init(__cs_mutex_t *__cs_m, int __cs_val)
                                        {
                                        *__cs_m = -1;
                                        return 0;
                                        }
                                        int __cs_mutex_destroy(__cs_mutex_t *__cs_mutex_to_destroy)
                                        {
                                        __CPROVER_assert((*__cs_mutex_to_destroy) != 0, "attempt to destroy an uninitialized mutex");
                                        __CPROVER_assert((*__cs_mutex_to_destroy) != (-2), "attempt to destroy a previously destroyed mutex");
                                        __CPROVER_assert((*__cs_mutex_to_destroy) == (-1), "attempt to destroy a locked mutex");
                                        *__cs_mutex_to_destroy = -2;
                                        __CSEQ_message("lock destroyed");
                                        return 0;
                                        }
                                        int __cs_mutex_lock(__cs_mutex_t *__cs_mutex_to_lock)
                                        {
                                        __CPROVER_assert((*__cs_mutex_to_lock) != 0, "attempt to lock an uninitialized mutex");
                                        __CPROVER_assert((*__cs_mutex_to_lock) != (-2), "attempt to lock a destroyed mutex");
                                        __CPROVER_assume((*__cs_mutex_to_lock) == (-1));
                                        *__cs_mutex_to_lock = __cs_thread_index + 1;
                                        __CSEQ_message("lock acquired");
                                        return 0;
                                        }
                                        int __cs_mutex_unlock(__cs_mutex_t *__cs_mutex_to_unlock)
                                        {
                                        __CPROVER_assert((*__cs_mutex_to_unlock) != 0, "attempt to unlock an uninitialized mutex");
                                        __CPROVER_assert((*__cs_mutex_to_unlock) != (-2), "attempt to unlock a destroyed mutex");
                                        __CPROVER_assert((*__cs_mutex_to_unlock) == (__cs_thread_index + 1), "attempt to release a lock held by another thread");
                                        *__cs_mutex_to_unlock = -1;
                                        __CSEQ_message("lock released");
                                        return 0;
                                        }
                                        typedef int __cs_cond_t;
                                        int __cs_cond_init(__cs_cond_t *__cs_cond_to_init, void *__cs_attr)
                                        {
                                        *__cs_cond_to_init = -1;
                                        return 0;
                                        }
                                        int __cs_cond_wait_1(__cs_cond_t *__cs_cond_to_wait_for, __cs_mutex_t *__cs_m)
                                        {
                                        __CPROVER_assert((*__cs_cond_to_wait_for) != 0, "attempt to use an uninitialized conditional variable");
                                        __CPROVER_assert((*__cs_cond_to_wait_for) != (-2), "attempt to use a destroyed conditional variable");
                                        __cs_mutex_unlock(__cs_m);
                                        }
                                        int __cs_cond_wait_2(__cs_cond_t *__cs_cond_to_wait_for, __cs_mutex_t *__cs_m)
                                        {
                                        __CPROVER_assume((*__cs_cond_to_wait_for) == 1);
                                        __cs_mutex_lock(__cs_m);
                                        return 0;
                                        }
                                        int __cs_cond_signal(__cs_cond_t *__cs_cond_to_signal)
                                        {
                                        *__cs_cond_to_signal = 1;
                                        __CSEQ_message("conditional variable signal");
                                        return 0;
                                        }
                                        extern void __VERIFIER_error();
                                        void __CSEQ_atomic_acquire(int *__cs_param___CSEQ_atomic_acquire_m)
                                        {
                                        __CPROVER_assume((*__cs_param___CSEQ_atomic_acquire_m) == 0);
                                        *__cs_param___CSEQ_atomic_acquire_m = 1;
                                        }
                                        void __CSEQ_atomic_release(int *__cs_param___CSEQ_atomic_release_m)
                                        {
                                        __CPROVER_assume((*__cs_param___CSEQ_atomic_release_m) == 1);
                                        *__cs_param___CSEQ_atomic_release_m = 0;
                                        }
                                        int memory[(2 * 320) + 1];
                                        int next_alloc_idx = 1;
                                        int m = 0;
                                        int top;
                                        void __CSEQ_atomic_assert(int __cs_param___CSEQ_atomic_assert_r)
                                        {
                                        		{
                                        static _Bool __cs_local___CSEQ_atomic_assert___cs_tmp_if_cond_3;
                                        __cs_init_scalar(&__cs_local___CSEQ_atomic_assert___cs_tmp_if_cond_3, sizeof(_Bool));
                                        static int __cs_retval__isEmpty_1;
                                        				{
                                        static _Bool __cs_local_isEmpty___cs_tmp_if_cond_1;
                                        __cs_init_scalar(&__cs_local_isEmpty___cs_tmp_if_cond_1, sizeof(_Bool));
                                        __cs_local_isEmpty___cs_tmp_if_cond_1 = top == 0;
                                        if (__cs_local_isEmpty___cs_tmp_if_cond_1)
                                        						{
                                        __cs_retval__isEmpty_1 = 1;
                                        goto __exit__isEmpty_1;
                                        								;
                                        						}
                                        						else
                                        						{
                                        __cs_retval__isEmpty_1 = 0;
                                        goto __exit__isEmpty_1;
                                        								;
                                        						}
                                        						;
                                        __exit__isEmpty_1:
                                        						__CPROVER_assume(__cs_pc_cs[0] >= 0);
                                        						;
                                        						;
                                        				}
                                        				;
                                        __cs_local___CSEQ_atomic_assert___cs_tmp_if_cond_3 = !(!((!__cs_param___CSEQ_atomic_assert_r) || (!__cs_retval__isEmpty_1)));
                                        if (__cs_local___CSEQ_atomic_assert___cs_tmp_if_cond_3)
                                        				{
                                        assert(0);
                                        (void) 0;
                                        				}
                                        				;
                                        		}
                                        		;
                                        		;
                                        		;
                                        }
                                        int m2 = 0;
                                        int state = 0;
                                        void *thr1_0(void *__cs_param_thr1_arg)
                                        {
IF(1,0,tthr1_0_1)
                                        __CSEQ_atomic_acquire(&m2);
                                        		;
                                        		;
                                        static int __cs_local_thr1___cs_switch_cond_1;
tthr1_0_1: IF(1,1,tthr1_0_2)
                                        __cs_local_thr1___cs_switch_cond_1 = state;
                                        		{
                                        static _Bool __cs_local_thr1___cs_tmp_if_cond_4;
                                        __cs_init_scalar(&__cs_local_thr1___cs_tmp_if_cond_4, sizeof(_Bool));
                                        __cs_local_thr1___cs_tmp_if_cond_4 = 0 || (__cs_local_thr1___cs_switch_cond_1 == 0);
                                        if (__cs_local_thr1___cs_tmp_if_cond_4)
                                        				{
                                        						{
tthr1_0_2: IF(1,2,tthr1_0_3)
                                        top = 0;
                                        __exit__EBStack_init_1:
                                        								__CPROVER_assume(__cs_pc_cs[1] >= 3);
                                        								;
                                        								;
                                        						}
                                        						;
tthr1_0_3: IF(1,3,tthr1_0_4)
                                        state = 1;
                                        				}
                                        __CPROVER_assume(__cs_pc_cs[1] >= 4);
                                        				;
                                        static _Bool __cs_local_thr1___cs_tmp_if_cond_5;
                                        __cs_init_scalar(&__cs_local_thr1___cs_tmp_if_cond_5, sizeof(_Bool));
                                        __cs_local_thr1___cs_tmp_if_cond_5 = (0 || (__cs_local_thr1___cs_switch_cond_1 == 0)) || (__cs_local_thr1___cs_switch_cond_1 == 1);
                                        if (__cs_local_thr1___cs_tmp_if_cond_5)
                                        				{
tthr1_0_4: IF(1,4,tthr1_0_5)
                                        __CSEQ_atomic_release(&m2);
                                        						{
                                        static int __cs_local_push_loop_r;
                                        __cs_init_scalar(&__cs_local_push_loop_r, sizeof(int));
                                        __cs_local_push_loop_r = -1;
                                        static int __cs_local_push_loop_arg;
                                        __cs_init_scalar(&__cs_local_push_loop_arg, sizeof(int));
                                        __cs_local_push_loop_arg = __VERIFIER_nondet_int();
                                        								{
                                        static int __cs_retval__push_1;
                                        										{
                                        static int __cs_param_push_d;
                                        __cs_param_push_d = __cs_local_push_loop_arg;
                                        static int __cs_local_push_oldTop;
                                        __cs_init_scalar(&__cs_local_push_oldTop, sizeof(int));
                                        __cs_local_push_oldTop = -1;
                                        static int __cs_local_push_newTop;
                                        __cs_init_scalar(&__cs_local_push_newTop, sizeof(int));
                                        __cs_local_push_newTop = -1;
                                        static int __cs_retval__index_malloc_1;
                                        												{
                                        static int __cs_local_index_malloc_curr_alloc_idx;
                                        __cs_init_scalar(&__cs_local_index_malloc_curr_alloc_idx, sizeof(int));
                                        __cs_local_index_malloc_curr_alloc_idx = -1;
tthr1_0_5: IF(1,5,tthr1_0_6)
                                        __CSEQ_atomic_acquire(&m);
                                        static _Bool __cs_local_index_malloc___cs_tmp_if_cond_0;
                                        __cs_init_scalar(&__cs_local_index_malloc___cs_tmp_if_cond_0, sizeof(_Bool));
tthr1_0_6: IF(1,6,tthr1_0_7)
                                        __cs_local_index_malloc___cs_tmp_if_cond_0 = ((next_alloc_idx + 2) - 1) > ((2 * 320) + 1);
                                        if (__cs_local_index_malloc___cs_tmp_if_cond_0)
                                        														{
tthr1_0_7: IF(1,7,tthr1_0_8)
                                        __CSEQ_atomic_release(&m);
                                        __cs_local_index_malloc_curr_alloc_idx = 0;
                                        														}
                                        														else
                                        														{
                                        __CPROVER_assume(__cs_pc_cs[1] >= 8);
tthr1_0_8: IF(1,8,tthr1_0_9)
                                        __cs_local_index_malloc_curr_alloc_idx = next_alloc_idx;
tthr1_0_9: IF(1,9,tthr1_0_10)
                                        next_alloc_idx += 2;
tthr1_0_10: IF(1,10,tthr1_0_11)
                                        __CSEQ_atomic_release(&m);
                                        														}
                                        __CPROVER_assume(__cs_pc_cs[1] >= 11);
                                        														;
                                        __cs_retval__index_malloc_1 = __cs_local_index_malloc_curr_alloc_idx;
                                        goto __exit__index_malloc_1_0;
                                        														;
                                        __exit__index_malloc_1_0:
                                        														__CPROVER_assume(__cs_pc_cs[1] >= 11);
                                        														;
                                        														;
                                        												}
                                        												;
                                        __cs_local_push_newTop = __cs_retval__index_malloc_1;
                                        static _Bool __cs_local_push___cs_tmp_if_cond_2;
                                        __cs_init_scalar(&__cs_local_push___cs_tmp_if_cond_2, sizeof(_Bool));
                                        __cs_local_push___cs_tmp_if_cond_2 = __cs_local_push_newTop == 0;
                                        if (__cs_local_push___cs_tmp_if_cond_2)
                                        												{
                                        __cs_retval__push_1 = 0;
                                        goto __exit__push_1_0;
                                        														;
                                        												}
                                        												else
                                        												{
tthr1_0_11: IF(1,11,tthr1_0_12)
                                        memory[__cs_local_push_newTop + 0] = __cs_param_push_d;
tthr1_0_12: IF(1,12,tthr1_0_13)
                                        __CSEQ_atomic_acquire(&m);
tthr1_0_13: IF(1,13,tthr1_0_14)
                                        __cs_local_push_oldTop = top;
tthr1_0_14: IF(1,14,tthr1_0_15)
                                        memory[__cs_local_push_newTop + 1] = __cs_local_push_oldTop;
tthr1_0_15: IF(1,15,tthr1_0_16)
                                        top = __cs_local_push_newTop;
tthr1_0_16: IF(1,16,tthr1_0_17)
                                        __CSEQ_atomic_release(&m);
                                        __cs_retval__push_1 = 1;
                                        goto __exit__push_1_0;
                                        														;
                                        												}
                                        __CPROVER_assume(__cs_pc_cs[1] >= 17);
                                        												;
                                        __exit__push_1_0:
                                        												__CPROVER_assume(__cs_pc_cs[1] >= 17);
                                        												;
                                        												;
                                        										}
                                        										;
                                        __cs_local_push_loop_r = __cs_retval__push_1;
tthr1_0_17: IF(1,17,tthr1_0_18)
                                        __CSEQ_atomic_assert(__cs_local_push_loop_r);
                                        								}
                                        								;
                                        								{
                                        static int __cs_retval__push_1;
                                        										{
                                        static int __cs_param_push_d;
                                        __cs_param_push_d = __cs_local_push_loop_arg;
                                        static int __cs_local_push_oldTop;
                                        __cs_init_scalar(&__cs_local_push_oldTop, sizeof(int));
                                        __cs_local_push_oldTop = -1;
                                        static int __cs_local_push_newTop;
                                        __cs_init_scalar(&__cs_local_push_newTop, sizeof(int));
                                        __cs_local_push_newTop = -1;
                                        static int __cs_retval__index_malloc_1;
                                        												{
                                        static int __cs_local_index_malloc_curr_alloc_idx;
                                        __cs_init_scalar(&__cs_local_index_malloc_curr_alloc_idx, sizeof(int));
                                        __cs_local_index_malloc_curr_alloc_idx = -1;
tthr1_0_18: IF(1,18,tthr1_0_19)
                                        __CSEQ_atomic_acquire(&m);
                                        static _Bool __cs_local_index_malloc___cs_tmp_if_cond_0;
                                        __cs_init_scalar(&__cs_local_index_malloc___cs_tmp_if_cond_0, sizeof(_Bool));
tthr1_0_19: IF(1,19,tthr1_0_20)
                                        __cs_local_index_malloc___cs_tmp_if_cond_0 = ((next_alloc_idx + 2) - 1) > ((2 * 320) + 1);
                                        if (__cs_local_index_malloc___cs_tmp_if_cond_0)
                                        														{
tthr1_0_20: IF(1,20,tthr1_0_21)
                                        __CSEQ_atomic_release(&m);
                                        __cs_local_index_malloc_curr_alloc_idx = 0;
                                        														}
                                        														else
                                        														{
                                        __CPROVER_assume(__cs_pc_cs[1] >= 21);
tthr1_0_21: IF(1,21,tthr1_0_22)
                                        __cs_local_index_malloc_curr_alloc_idx = next_alloc_idx;
tthr1_0_22: IF(1,22,tthr1_0_23)
                                        next_alloc_idx += 2;
tthr1_0_23: IF(1,23,tthr1_0_24)
                                        __CSEQ_atomic_release(&m);
                                        														}
                                        __CPROVER_assume(__cs_pc_cs[1] >= 24);
                                        														;
                                        __cs_retval__index_malloc_1 = __cs_local_index_malloc_curr_alloc_idx;
                                        goto __exit__index_malloc_1_1;
                                        														;
                                        __exit__index_malloc_1_1:
                                        														__CPROVER_assume(__cs_pc_cs[1] >= 24);
                                        														;
                                        														;
                                        												}
                                        												;
                                        __cs_local_push_newTop = __cs_retval__index_malloc_1;
                                        static _Bool __cs_local_push___cs_tmp_if_cond_2;
                                        __cs_init_scalar(&__cs_local_push___cs_tmp_if_cond_2, sizeof(_Bool));
                                        __cs_local_push___cs_tmp_if_cond_2 = __cs_local_push_newTop == 0;
                                        if (__cs_local_push___cs_tmp_if_cond_2)
                                        												{
                                        __cs_retval__push_1 = 0;
                                        goto __exit__push_1_1;
                                        														;
                                        												}
                                        												else
                                        												{
tthr1_0_24: IF(1,24,tthr1_0_25)
                                        memory[__cs_local_push_newTop + 0] = __cs_param_push_d;
tthr1_0_25: IF(1,25,tthr1_0_26)
                                        __CSEQ_atomic_acquire(&m);
tthr1_0_26: IF(1,26,tthr1_0_27)
                                        __cs_local_push_oldTop = top;
tthr1_0_27: IF(1,27,tthr1_0_28)
                                        memory[__cs_local_push_newTop + 1] = __cs_local_push_oldTop;
tthr1_0_28: IF(1,28,tthr1_0_29)
                                        top = __cs_local_push_newTop;
tthr1_0_29: IF(1,29,tthr1_0_30)
                                        __CSEQ_atomic_release(&m);
                                        __cs_retval__push_1 = 1;
                                        goto __exit__push_1_1;
                                        														;
                                        												}
                                        __CPROVER_assume(__cs_pc_cs[1] >= 30);
                                        												;
                                        __exit__push_1_1:
                                        												__CPROVER_assume(__cs_pc_cs[1] >= 30);
                                        												;
                                        												;
                                        										}
                                        										;
                                        __cs_local_push_loop_r = __cs_retval__push_1;
tthr1_0_30: IF(1,30,tthr1_0_31)
                                        __CSEQ_atomic_assert(__cs_local_push_loop_r);
                                        								}
                                        								;
tthr1_0_31: IF(1,31,tthr1_0_32)
                                        __CPROVER_assume(!1);
                                        __exit_loop_1:
                                        								__CPROVER_assume(__cs_pc_cs[1] >= 32);
                                        								;
                                        								;
                                        __exit__push_loop_1:
                                        								__CPROVER_assume(__cs_pc_cs[1] >= 32);
                                        								;
                                        								;
                                        						}
                                        						;
                                        				}
                                        __CPROVER_assume(__cs_pc_cs[1] >= 32);
                                        				;
                                        		}
                                        		;
                                        __cs_switch_exit_1:
                                        		__CPROVER_assume(__cs_pc_cs[1] >= 32);
                                        		;
                                        		;
                                        goto __exit_thr1;
                                        		;
                                        __exit_thr1:
                                        		__CPROVER_assume(__cs_pc_cs[1] >= 32);
                                        		;
                                        		;
tthr1_0_32: 
                                        STOP_NONVOID(32);
                                        }
                                        void *thr1_1(void *__cs_param_thr1_arg)
                                        {
IF(2,0,tthr1_1_1)
                                        __CSEQ_atomic_acquire(&m2);
                                        		;
                                        		;
                                        static int __cs_local_thr1___cs_switch_cond_1;
tthr1_1_1: IF(2,1,tthr1_1_2)
                                        __cs_local_thr1___cs_switch_cond_1 = state;
                                        		{
                                        static _Bool __cs_local_thr1___cs_tmp_if_cond_4;
                                        __cs_init_scalar(&__cs_local_thr1___cs_tmp_if_cond_4, sizeof(_Bool));
                                        __cs_local_thr1___cs_tmp_if_cond_4 = 0 || (__cs_local_thr1___cs_switch_cond_1 == 0);
                                        if (__cs_local_thr1___cs_tmp_if_cond_4)
                                        				{
                                        						{
tthr1_1_2: IF(2,2,tthr1_1_3)
                                        top = 0;
                                        __exit__EBStack_init_1:
                                        								__CPROVER_assume(__cs_pc_cs[2] >= 3);
                                        								;
                                        								;
                                        						}
                                        						;
tthr1_1_3: IF(2,3,tthr1_1_4)
                                        state = 1;
                                        				}
                                        __CPROVER_assume(__cs_pc_cs[2] >= 4);
                                        				;
                                        static _Bool __cs_local_thr1___cs_tmp_if_cond_5;
                                        __cs_init_scalar(&__cs_local_thr1___cs_tmp_if_cond_5, sizeof(_Bool));
                                        __cs_local_thr1___cs_tmp_if_cond_5 = (0 || (__cs_local_thr1___cs_switch_cond_1 == 0)) || (__cs_local_thr1___cs_switch_cond_1 == 1);
                                        if (__cs_local_thr1___cs_tmp_if_cond_5)
                                        				{
tthr1_1_4: IF(2,4,tthr1_1_5)
                                        __CSEQ_atomic_release(&m2);
                                        						{
                                        static int __cs_local_push_loop_r;
                                        __cs_init_scalar(&__cs_local_push_loop_r, sizeof(int));
                                        __cs_local_push_loop_r = -1;
                                        static int __cs_local_push_loop_arg;
                                        __cs_init_scalar(&__cs_local_push_loop_arg, sizeof(int));
                                        __cs_local_push_loop_arg = __VERIFIER_nondet_int();
                                        								{
                                        static int __cs_retval__push_1;
                                        										{
                                        static int __cs_param_push_d;
                                        __cs_param_push_d = __cs_local_push_loop_arg;
                                        static int __cs_local_push_oldTop;
                                        __cs_init_scalar(&__cs_local_push_oldTop, sizeof(int));
                                        __cs_local_push_oldTop = -1;
                                        static int __cs_local_push_newTop;
                                        __cs_init_scalar(&__cs_local_push_newTop, sizeof(int));
                                        __cs_local_push_newTop = -1;
                                        static int __cs_retval__index_malloc_1;
                                        												{
                                        static int __cs_local_index_malloc_curr_alloc_idx;
                                        __cs_init_scalar(&__cs_local_index_malloc_curr_alloc_idx, sizeof(int));
                                        __cs_local_index_malloc_curr_alloc_idx = -1;
tthr1_1_5: IF(2,5,tthr1_1_6)
                                        __CSEQ_atomic_acquire(&m);
                                        static _Bool __cs_local_index_malloc___cs_tmp_if_cond_0;
                                        __cs_init_scalar(&__cs_local_index_malloc___cs_tmp_if_cond_0, sizeof(_Bool));
tthr1_1_6: IF(2,6,tthr1_1_7)
                                        __cs_local_index_malloc___cs_tmp_if_cond_0 = ((next_alloc_idx + 2) - 1) > ((2 * 320) + 1);
                                        if (__cs_local_index_malloc___cs_tmp_if_cond_0)
                                        														{
tthr1_1_7: IF(2,7,tthr1_1_8)
                                        __CSEQ_atomic_release(&m);
                                        __cs_local_index_malloc_curr_alloc_idx = 0;
                                        														}
                                        														else
                                        														{
                                        __CPROVER_assume(__cs_pc_cs[2] >= 8);
tthr1_1_8: IF(2,8,tthr1_1_9)
                                        __cs_local_index_malloc_curr_alloc_idx = next_alloc_idx;
tthr1_1_9: IF(2,9,tthr1_1_10)
                                        next_alloc_idx += 2;
tthr1_1_10: IF(2,10,tthr1_1_11)
                                        __CSEQ_atomic_release(&m);
                                        														}
                                        __CPROVER_assume(__cs_pc_cs[2] >= 11);
                                        														;
                                        __cs_retval__index_malloc_1 = __cs_local_index_malloc_curr_alloc_idx;
                                        goto __exit__index_malloc_1_0;
                                        														;
                                        __exit__index_malloc_1_0:
                                        														__CPROVER_assume(__cs_pc_cs[2] >= 11);
                                        														;
                                        														;
                                        												}
                                        												;
                                        __cs_local_push_newTop = __cs_retval__index_malloc_1;
                                        static _Bool __cs_local_push___cs_tmp_if_cond_2;
                                        __cs_init_scalar(&__cs_local_push___cs_tmp_if_cond_2, sizeof(_Bool));
                                        __cs_local_push___cs_tmp_if_cond_2 = __cs_local_push_newTop == 0;
                                        if (__cs_local_push___cs_tmp_if_cond_2)
                                        												{
                                        __cs_retval__push_1 = 0;
                                        goto __exit__push_1_0;
                                        														;
                                        												}
                                        												else
                                        												{
tthr1_1_11: IF(2,11,tthr1_1_12)
                                        memory[__cs_local_push_newTop + 0] = __cs_param_push_d;
tthr1_1_12: IF(2,12,tthr1_1_13)
                                        __CSEQ_atomic_acquire(&m);
tthr1_1_13: IF(2,13,tthr1_1_14)
                                        __cs_local_push_oldTop = top;
tthr1_1_14: IF(2,14,tthr1_1_15)
                                        memory[__cs_local_push_newTop + 1] = __cs_local_push_oldTop;
tthr1_1_15: IF(2,15,tthr1_1_16)
                                        top = __cs_local_push_newTop;
tthr1_1_16: IF(2,16,tthr1_1_17)
                                        __CSEQ_atomic_release(&m);
                                        __cs_retval__push_1 = 1;
                                        goto __exit__push_1_0;
                                        														;
                                        												}
                                        __CPROVER_assume(__cs_pc_cs[2] >= 17);
                                        												;
                                        __exit__push_1_0:
                                        												__CPROVER_assume(__cs_pc_cs[2] >= 17);
                                        												;
                                        												;
                                        										}
                                        										;
                                        __cs_local_push_loop_r = __cs_retval__push_1;
tthr1_1_17: IF(2,17,tthr1_1_18)
                                        __CSEQ_atomic_assert(__cs_local_push_loop_r);
                                        								}
                                        								;
                                        								{
                                        static int __cs_retval__push_1;
                                        										{
                                        static int __cs_param_push_d;
                                        __cs_param_push_d = __cs_local_push_loop_arg;
                                        static int __cs_local_push_oldTop;
                                        __cs_init_scalar(&__cs_local_push_oldTop, sizeof(int));
                                        __cs_local_push_oldTop = -1;
                                        static int __cs_local_push_newTop;
                                        __cs_init_scalar(&__cs_local_push_newTop, sizeof(int));
                                        __cs_local_push_newTop = -1;
                                        static int __cs_retval__index_malloc_1;
                                        												{
                                        static int __cs_local_index_malloc_curr_alloc_idx;
                                        __cs_init_scalar(&__cs_local_index_malloc_curr_alloc_idx, sizeof(int));
                                        __cs_local_index_malloc_curr_alloc_idx = -1;
tthr1_1_18: IF(2,18,tthr1_1_19)
                                        __CSEQ_atomic_acquire(&m);
                                        static _Bool __cs_local_index_malloc___cs_tmp_if_cond_0;
                                        __cs_init_scalar(&__cs_local_index_malloc___cs_tmp_if_cond_0, sizeof(_Bool));
tthr1_1_19: IF(2,19,tthr1_1_20)
                                        __cs_local_index_malloc___cs_tmp_if_cond_0 = ((next_alloc_idx + 2) - 1) > ((2 * 320) + 1);
                                        if (__cs_local_index_malloc___cs_tmp_if_cond_0)
                                        														{
tthr1_1_20: IF(2,20,tthr1_1_21)
                                        __CSEQ_atomic_release(&m);
                                        __cs_local_index_malloc_curr_alloc_idx = 0;
                                        														}
                                        														else
                                        														{
                                        __CPROVER_assume(__cs_pc_cs[2] >= 21);
tthr1_1_21: IF(2,21,tthr1_1_22)
                                        __cs_local_index_malloc_curr_alloc_idx = next_alloc_idx;
tthr1_1_22: IF(2,22,tthr1_1_23)
                                        next_alloc_idx += 2;
tthr1_1_23: IF(2,23,tthr1_1_24)
                                        __CSEQ_atomic_release(&m);
                                        														}
                                        __CPROVER_assume(__cs_pc_cs[2] >= 24);
                                        														;
                                        __cs_retval__index_malloc_1 = __cs_local_index_malloc_curr_alloc_idx;
                                        goto __exit__index_malloc_1_1;
                                        														;
                                        __exit__index_malloc_1_1:
                                        														__CPROVER_assume(__cs_pc_cs[2] >= 24);
                                        														;
                                        														;
                                        												}
                                        												;
                                        __cs_local_push_newTop = __cs_retval__index_malloc_1;
                                        static _Bool __cs_local_push___cs_tmp_if_cond_2;
                                        __cs_init_scalar(&__cs_local_push___cs_tmp_if_cond_2, sizeof(_Bool));
                                        __cs_local_push___cs_tmp_if_cond_2 = __cs_local_push_newTop == 0;
                                        if (__cs_local_push___cs_tmp_if_cond_2)
                                        												{
                                        __cs_retval__push_1 = 0;
                                        goto __exit__push_1_1;
                                        														;
                                        												}
                                        												else
                                        												{
tthr1_1_24: IF(2,24,tthr1_1_25)
                                        memory[__cs_local_push_newTop + 0] = __cs_param_push_d;
tthr1_1_25: IF(2,25,tthr1_1_26)
                                        __CSEQ_atomic_acquire(&m);
tthr1_1_26: IF(2,26,tthr1_1_27)
                                        __cs_local_push_oldTop = top;
tthr1_1_27: IF(2,27,tthr1_1_28)
                                        memory[__cs_local_push_newTop + 1] = __cs_local_push_oldTop;
tthr1_1_28: IF(2,28,tthr1_1_29)
                                        top = __cs_local_push_newTop;
tthr1_1_29: IF(2,29,tthr1_1_30)
                                        __CSEQ_atomic_release(&m);
                                        __cs_retval__push_1 = 1;
                                        goto __exit__push_1_1;
                                        														;
                                        												}
                                        __CPROVER_assume(__cs_pc_cs[2] >= 30);
                                        												;
                                        __exit__push_1_1:
                                        												__CPROVER_assume(__cs_pc_cs[2] >= 30);
                                        												;
                                        												;
                                        										}
                                        										;
                                        __cs_local_push_loop_r = __cs_retval__push_1;
tthr1_1_30: IF(2,30,tthr1_1_31)
                                        __CSEQ_atomic_assert(__cs_local_push_loop_r);
                                        								}
                                        								;
tthr1_1_31: IF(2,31,tthr1_1_32)
                                        __CPROVER_assume(!1);
                                        __exit_loop_1:
                                        								__CPROVER_assume(__cs_pc_cs[2] >= 32);
                                        								;
                                        								;
                                        __exit__push_loop_1:
                                        								__CPROVER_assume(__cs_pc_cs[2] >= 32);
                                        								;
                                        								;
                                        						}
                                        						;
                                        				}
                                        __CPROVER_assume(__cs_pc_cs[2] >= 32);
                                        				;
                                        		}
                                        		;
                                        __cs_switch_exit_1:
                                        		__CPROVER_assume(__cs_pc_cs[2] >= 32);
                                        		;
                                        		;
                                        goto __exit_thr1;
                                        		;
                                        __exit_thr1:
                                        		__CPROVER_assume(__cs_pc_cs[2] >= 32);
                                        		;
                                        		;
tthr1_1_32: 
                                        STOP_NONVOID(32);
                                        }
                                        int main_thread(void)
                                        {
                                        		;
IF(0,0,tmain_1)
                                        static __cs_t __cs_local_main_t;
                                        __cs_init_scalar(&__cs_local_main_t, sizeof(__cs_t));
                                        		{
                                        __cs_create(&__cs_local_main_t, 0, thr1_0, 0, 1);
                                        		}
                                        		;
                                        		{
tmain_1: IF(0,1,tmain_2)
                                        __cs_create(&__cs_local_main_t, 0, thr1_1, 0, 2);
                                        		}
                                        		;
tmain_2: IF(0,2,tmain_3)
                                        __CPROVER_assume(!1);
                                        __exit_loop_2:
                                        		__CPROVER_assume(__cs_pc_cs[0] >= 3);
                                        		;
                                        		;
                                        __exit_main:
                                        		__CPROVER_assume(__cs_pc_cs[0] >= 3);
                                        		;
                                        		;
tmain_3: 
                                        STOP_NONVOID(3);
                                        }
                                        int main(void)
                                        {
                                        unsigned __CPROVER_bitvector[2] __cs_tmp_t0_r0 = (unsigned __CPROVER_bitvector[2])nondet_uint();
                                        unsigned __CPROVER_bitvector[6] __cs_tmp_t1_r0 = (unsigned __CPROVER_bitvector[6])nondet_uint();
                                        unsigned __CPROVER_bitvector[6] __cs_tmp_t2_r0 = (unsigned __CPROVER_bitvector[6])nondet_uint();
                                        unsigned __CPROVER_bitvector[2] __cs_tmp_t0_r1 = (unsigned __CPROVER_bitvector[2])nondet_uint();
/* round  0 */
                                        __CPROVER_assume(__cs_tmp_t0_r0 > 0);
                                        __cs_thread_index = 0;
                                        __cs_pc_cs[0] = __cs_pc[0] + __cs_tmp_t0_r0;
                                        __CPROVER_assume(__cs_pc_cs[0] > 0);
                                        __CPROVER_assume(__cs_pc_cs[0] <= 3);
                                        main_thread();
                                        __cs_pc[0] = __cs_pc_cs[0];
                                        if (__cs_active_thread[1] == 1)
                                        		{
                                        __cs_thread_index = 1;
                                        __cs_pc_cs[1] = __cs_pc[1] + __cs_tmp_t1_r0;
                                        __CPROVER_assume(__cs_pc_cs[1] <= 32);
                                        thr1_0(__cs_threadargs[1]);
                                        __cs_pc[1] = __cs_pc_cs[1];
                                        		}
                                        if (__cs_active_thread[2] == 1)
                                        		{
                                        __cs_thread_index = 2;
                                        __cs_pc_cs[2] = __cs_pc[2] + __cs_tmp_t2_r0;
                                        __CPROVER_assume(__cs_pc_cs[2] <= 32);
                                        thr1_1(__cs_threadargs[2]);
                                        __cs_pc[2] = __cs_pc_cs[2];
                                        		}
                                        if (__cs_active_thread[0] == 1)
                                        		{
                                        __cs_thread_index = 0;
                                        __cs_pc_cs[0] = __cs_pc[0] + __cs_tmp_t0_r1;
                                        __CPROVER_assume(__cs_pc_cs[0] >= __cs_pc[0]);
                                        __CPROVER_assume(__cs_pc_cs[0] <= 3);
                                        main_thread();
                                        		}
                                        return 0;
                                        }
                                        
