	.file	"342819.c"
	.intel_syntax noprefix
	.text
	.globl	__VERIFIER_assert
	.type	__VERIFIER_assert, @function
__VERIFIER_assert:
.LFB0:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	sub	rsp, 16
	mov	DWORD PTR -4[rbp], edi
	cmp	DWORD PTR -4[rbp], 0
	jne	.L5
	nop
.L3:
	mov	eax, 0
	call	__VERIFIER_error@PLT
.L5:
	nop
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE0:
	.size	__VERIFIER_assert, .-__VERIFIER_assert
	.globl	__global_lock
	.bss
	.align 4
	.type	__global_lock, @object
	.size	__global_lock, 4
__global_lock:
	.zero	4
	.text
	.globl	__VERIFIER_atomic_begin
	.type	__VERIFIER_atomic_begin, @function
__VERIFIER_atomic_begin:
.LFB1:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	mov	eax, DWORD PTR __global_lock[rip]
	test	eax, eax
	sete	al
	movzx	eax, al
	mov	edi, eax
	mov	eax, 0
	call	__VERIFIER_assume@PLT
	mov	DWORD PTR __global_lock[rip], 1
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE1:
	.size	__VERIFIER_atomic_begin, .-__VERIFIER_atomic_begin
	.globl	__VERIFIER_atomic_end
	.type	__VERIFIER_atomic_end, @function
__VERIFIER_atomic_end:
.LFB2:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	mov	eax, DWORD PTR __global_lock[rip]
	cmp	eax, 1
	sete	al
	movzx	eax, al
	mov	edi, eax
	mov	eax, 0
	call	__VERIFIER_assume@PLT
	mov	DWORD PTR __global_lock[rip], 0
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE2:
	.size	__VERIFIER_atomic_end, .-__VERIFIER_atomic_end
	.globl	__unbuffered_cnt
	.bss
	.align 4
	.type	__unbuffered_cnt, @object
	.size	__unbuffered_cnt, 4
__unbuffered_cnt:
	.zero	4
	.globl	__unbuffered_p0_EAX
	.align 4
	.type	__unbuffered_p0_EAX, @object
	.size	__unbuffered_p0_EAX, 4
__unbuffered_p0_EAX:
	.zero	4
	.globl	__unbuffered_p0_EBX
	.align 4
	.type	__unbuffered_p0_EBX, @object
	.size	__unbuffered_p0_EBX, 4
__unbuffered_p0_EBX:
	.zero	4
	.globl	__unbuffered_p1_EAX
	.align 4
	.type	__unbuffered_p1_EAX, @object
	.size	__unbuffered_p1_EAX, 4
__unbuffered_p1_EAX:
	.zero	4
	.globl	__unbuffered_p2_EAX
	.align 4
	.type	__unbuffered_p2_EAX, @object
	.size	__unbuffered_p2_EAX, 4
__unbuffered_p2_EAX:
	.zero	4
	.globl	__unbuffered_p2_EBX
	.align 4
	.type	__unbuffered_p2_EBX, @object
	.size	__unbuffered_p2_EBX, 4
__unbuffered_p2_EBX:
	.zero	4
	.globl	a
	.align 4
	.type	a, @object
	.size	a, 4
a:
	.zero	4
	.globl	a$flush_delayed
	.type	a$flush_delayed, @object
	.size	a$flush_delayed, 1
a$flush_delayed:
	.zero	1
	.globl	a$mem_tmp
	.align 4
	.type	a$mem_tmp, @object
	.size	a$mem_tmp, 4
a$mem_tmp:
	.zero	4
	.globl	a$r_buff0_thd0
	.type	a$r_buff0_thd0, @object
	.size	a$r_buff0_thd0, 1
a$r_buff0_thd0:
	.zero	1
	.globl	a$r_buff0_thd1
	.type	a$r_buff0_thd1, @object
	.size	a$r_buff0_thd1, 1
a$r_buff0_thd1:
	.zero	1
	.globl	a$r_buff0_thd2
	.type	a$r_buff0_thd2, @object
	.size	a$r_buff0_thd2, 1
a$r_buff0_thd2:
	.zero	1
	.globl	a$r_buff0_thd3
	.type	a$r_buff0_thd3, @object
	.size	a$r_buff0_thd3, 1
a$r_buff0_thd3:
	.zero	1
	.globl	a$r_buff1_thd0
	.type	a$r_buff1_thd0, @object
	.size	a$r_buff1_thd0, 1
a$r_buff1_thd0:
	.zero	1
	.globl	a$r_buff1_thd1
	.type	a$r_buff1_thd1, @object
	.size	a$r_buff1_thd1, 1
a$r_buff1_thd1:
	.zero	1
	.globl	a$r_buff1_thd2
	.type	a$r_buff1_thd2, @object
	.size	a$r_buff1_thd2, 1
a$r_buff1_thd2:
	.zero	1
	.globl	a$r_buff1_thd3
	.type	a$r_buff1_thd3, @object
	.size	a$r_buff1_thd3, 1
a$r_buff1_thd3:
	.zero	1
	.globl	a$read_delayed
	.type	a$read_delayed, @object
	.size	a$read_delayed, 1
a$read_delayed:
	.zero	1
	.globl	a$read_delayed_var
	.align 8
	.type	a$read_delayed_var, @object
	.size	a$read_delayed_var, 8
a$read_delayed_var:
	.zero	8
	.globl	a$w_buff0
	.align 4
	.type	a$w_buff0, @object
	.size	a$w_buff0, 4
a$w_buff0:
	.zero	4
	.globl	a$w_buff0_used
	.type	a$w_buff0_used, @object
	.size	a$w_buff0_used, 1
a$w_buff0_used:
	.zero	1
	.globl	a$w_buff1
	.align 4
	.type	a$w_buff1, @object
	.size	a$w_buff1, 4
a$w_buff1:
	.zero	4
	.globl	a$w_buff1_used
	.type	a$w_buff1_used, @object
	.size	a$w_buff1_used, 1
a$w_buff1_used:
	.zero	1
	.globl	main$tmp_guard0
	.type	main$tmp_guard0, @object
	.size	main$tmp_guard0, 1
main$tmp_guard0:
	.zero	1
	.globl	main$tmp_guard1
	.type	main$tmp_guard1, @object
	.size	main$tmp_guard1, 1
main$tmp_guard1:
	.zero	1
	.globl	x
	.align 4
	.type	x, @object
	.size	x, 4
x:
	.zero	4
	.globl	y
	.align 4
	.type	y, @object
	.size	y, 4
y:
	.zero	4
	.globl	z
	.align 4
	.type	z, @object
	.size	z, 4
z:
	.zero	4
	.globl	weak$$choice0
	.type	weak$$choice0, @object
	.size	weak$$choice0, 1
weak$$choice0:
	.zero	1
	.globl	weak$$choice2
	.type	weak$$choice2, @object
	.size	weak$$choice2, 1
weak$$choice2:
	.zero	1
	.text
	.globl	P0
	.type	P0, @function
P0:
.LFB3:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	sub	rsp, 16
	mov	QWORD PTR -8[rbp], rdi
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	mov	eax, DWORD PTR a$w_buff0[rip]
	mov	DWORD PTR a$w_buff1[rip], eax
	mov	DWORD PTR a$w_buff0[rip], 1
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	mov	BYTE PTR a$w_buff1_used[rip], al
	mov	BYTE PTR a$w_buff0_used[rip], 1
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L11
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	je	.L12
.L11:
	mov	eax, 1
	jmp	.L13
.L12:
	mov	eax, 0
.L13:
	mov	edi, eax
	call	__VERIFIER_assert
	movzx	eax, BYTE PTR a$r_buff0_thd0[rip]
	mov	BYTE PTR a$r_buff1_thd0[rip], al
	movzx	eax, BYTE PTR a$r_buff0_thd1[rip]
	mov	BYTE PTR a$r_buff1_thd1[rip], al
	movzx	eax, BYTE PTR a$r_buff0_thd2[rip]
	mov	BYTE PTR a$r_buff1_thd2[rip], al
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	mov	BYTE PTR a$r_buff1_thd3[rip], al
	mov	BYTE PTR a$r_buff0_thd1[rip], 1
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	mov	DWORD PTR x[rip], 1
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	mov	eax, DWORD PTR x[rip]
	mov	DWORD PTR __unbuffered_p0_EAX[rip], eax
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	mov	eax, DWORD PTR y[rip]
	mov	DWORD PTR __unbuffered_p0_EBX[rip], eax
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L14
	movzx	eax, BYTE PTR a$r_buff0_thd1[rip]
	test	al, al
	jne	.L15
.L14:
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	test	al, al
	je	.L16
	movzx	eax, BYTE PTR a$r_buff1_thd1[rip]
	test	al, al
	je	.L16
	mov	eax, DWORD PTR a$w_buff1[rip]
	jmp	.L18
.L16:
	mov	eax, DWORD PTR a[rip]
	jmp	.L18
.L15:
	mov	eax, DWORD PTR a$w_buff0[rip]
.L18:
	mov	DWORD PTR a[rip], eax
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L19
	movzx	eax, BYTE PTR a$r_buff0_thd1[rip]
	test	al, al
	jne	.L20
.L19:
	mov	eax, 1
	jmp	.L21
.L20:
	mov	eax, 0
.L21:
	and	eax, 1
	test	al, al
	je	.L22
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L22
	mov	eax, 1
	jmp	.L23
.L22:
	mov	eax, 0
.L23:
	mov	BYTE PTR a$w_buff0_used[rip], al
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L24
	movzx	eax, BYTE PTR a$r_buff0_thd1[rip]
	test	al, al
	jne	.L25
.L24:
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	test	al, al
	je	.L26
	movzx	eax, BYTE PTR a$r_buff1_thd1[rip]
	test	al, al
	jne	.L25
.L26:
	mov	eax, 1
	jmp	.L27
.L25:
	mov	eax, 0
.L27:
	and	eax, 1
	test	al, al
	je	.L28
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L28
	mov	eax, 1
	jmp	.L29
.L28:
	mov	eax, 0
.L29:
	mov	BYTE PTR a$w_buff1_used[rip], al
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L30
	movzx	eax, BYTE PTR a$r_buff0_thd1[rip]
	test	al, al
	jne	.L31
.L30:
	mov	eax, 1
	jmp	.L32
.L31:
	mov	eax, 0
.L32:
	and	eax, 1
	test	al, al
	je	.L33
	movzx	eax, BYTE PTR a$r_buff0_thd1[rip]
	movzx	eax, al
	test	eax, eax
	je	.L33
	mov	eax, 1
	jmp	.L34
.L33:
	mov	eax, 0
.L34:
	mov	BYTE PTR a$r_buff0_thd1[rip], al
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L35
	movzx	eax, BYTE PTR a$r_buff0_thd1[rip]
	test	al, al
	jne	.L36
.L35:
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	test	al, al
	je	.L37
	movzx	eax, BYTE PTR a$r_buff1_thd1[rip]
	test	al, al
	jne	.L36
.L37:
	mov	eax, 1
	jmp	.L38
.L36:
	mov	eax, 0
.L38:
	and	eax, 1
	test	al, al
	je	.L39
	movzx	eax, BYTE PTR a$r_buff1_thd1[rip]
	movzx	eax, al
	test	eax, eax
	je	.L39
	mov	eax, 1
	jmp	.L40
.L39:
	mov	eax, 0
.L40:
	mov	BYTE PTR a$r_buff1_thd1[rip], al
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	mov	eax, DWORD PTR __unbuffered_cnt[rip]
	add	eax, 1
	mov	DWORD PTR __unbuffered_cnt[rip], eax
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	nondet_0@PLT
	cdqe
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE3:
	.size	P0, .-P0
	.globl	P1
	.type	P1, @function
P1:
.LFB4:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	sub	rsp, 16
	mov	QWORD PTR -8[rbp], rdi
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	mov	DWORD PTR y[rip], 1
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	mov	eax, DWORD PTR z[rip]
	mov	DWORD PTR __unbuffered_p1_EAX[rip], eax
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L43
	movzx	eax, BYTE PTR a$r_buff0_thd2[rip]
	test	al, al
	jne	.L44
.L43:
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	test	al, al
	je	.L45
	movzx	eax, BYTE PTR a$r_buff1_thd2[rip]
	test	al, al
	je	.L45
	mov	eax, DWORD PTR a$w_buff1[rip]
	jmp	.L47
.L45:
	mov	eax, DWORD PTR a[rip]
	jmp	.L47
.L44:
	mov	eax, DWORD PTR a$w_buff0[rip]
.L47:
	mov	DWORD PTR a[rip], eax
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L48
	movzx	eax, BYTE PTR a$r_buff0_thd2[rip]
	test	al, al
	jne	.L49
.L48:
	mov	eax, 1
	jmp	.L50
.L49:
	mov	eax, 0
.L50:
	and	eax, 1
	test	al, al
	je	.L51
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L51
	mov	eax, 1
	jmp	.L52
.L51:
	mov	eax, 0
.L52:
	mov	BYTE PTR a$w_buff0_used[rip], al
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L53
	movzx	eax, BYTE PTR a$r_buff0_thd2[rip]
	test	al, al
	jne	.L54
.L53:
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	test	al, al
	je	.L55
	movzx	eax, BYTE PTR a$r_buff1_thd2[rip]
	test	al, al
	jne	.L54
.L55:
	mov	eax, 1
	jmp	.L56
.L54:
	mov	eax, 0
.L56:
	and	eax, 1
	test	al, al
	je	.L57
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L57
	mov	eax, 1
	jmp	.L58
.L57:
	mov	eax, 0
.L58:
	mov	BYTE PTR a$w_buff1_used[rip], al
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L59
	movzx	eax, BYTE PTR a$r_buff0_thd2[rip]
	test	al, al
	jne	.L60
.L59:
	mov	eax, 1
	jmp	.L61
.L60:
	mov	eax, 0
.L61:
	and	eax, 1
	test	al, al
	je	.L62
	movzx	eax, BYTE PTR a$r_buff0_thd2[rip]
	movzx	eax, al
	test	eax, eax
	je	.L62
	mov	eax, 1
	jmp	.L63
.L62:
	mov	eax, 0
.L63:
	mov	BYTE PTR a$r_buff0_thd2[rip], al
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L64
	movzx	eax, BYTE PTR a$r_buff0_thd2[rip]
	test	al, al
	jne	.L65
.L64:
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	test	al, al
	je	.L66
	movzx	eax, BYTE PTR a$r_buff1_thd2[rip]
	test	al, al
	jne	.L65
.L66:
	mov	eax, 1
	jmp	.L67
.L65:
	mov	eax, 0
.L67:
	and	eax, 1
	test	al, al
	je	.L68
	movzx	eax, BYTE PTR a$r_buff1_thd2[rip]
	movzx	eax, al
	test	eax, eax
	je	.L68
	mov	eax, 1
	jmp	.L69
.L68:
	mov	eax, 0
.L69:
	mov	BYTE PTR a$r_buff1_thd2[rip], al
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	mov	eax, DWORD PTR __unbuffered_cnt[rip]
	add	eax, 1
	mov	DWORD PTR __unbuffered_cnt[rip], eax
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	nondet_0@PLT
	cdqe
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE4:
	.size	P1, .-P1
	.globl	P2
	.type	P2, @function
P2:
.LFB5:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	sub	rsp, 16
	mov	QWORD PTR -8[rbp], rdi
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	mov	DWORD PTR z[rip], 1
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	mov	eax, DWORD PTR z[rip]
	mov	DWORD PTR __unbuffered_p2_EAX[rip], eax
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	mov	eax, 0
	call	nondet_1@PLT
	test	eax, eax
	setne	al
	mov	BYTE PTR weak$$choice0[rip], al
	mov	eax, 0
	call	nondet_1@PLT
	test	eax, eax
	setne	al
	mov	BYTE PTR weak$$choice2[rip], al
	movzx	eax, BYTE PTR weak$$choice2[rip]
	mov	BYTE PTR a$flush_delayed[rip], al
	mov	eax, DWORD PTR a[rip]
	mov	DWORD PTR a$mem_tmp[rip], eax
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L72
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	test	al, al
	jne	.L73
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	test	al, al
	je	.L72
.L73:
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	test	al, al
	jne	.L74
	movzx	eax, BYTE PTR a$r_buff1_thd3[rip]
	test	al, al
	je	.L72
.L74:
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L75
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	test	al, al
	je	.L75
	mov	eax, DWORD PTR a$w_buff0[rip]
	jmp	.L77
.L75:
	mov	eax, DWORD PTR a$w_buff1[rip]
	jmp	.L77
.L72:
	mov	eax, DWORD PTR a[rip]
.L77:
	mov	DWORD PTR a[rip], eax
	mov	eax, DWORD PTR a$w_buff0[rip]
	mov	DWORD PTR a$w_buff0[rip], eax
	mov	eax, DWORD PTR a$w_buff1[rip]
	mov	DWORD PTR a$w_buff1[rip], eax
	movzx	eax, BYTE PTR weak$$choice2[rip]
	test	al, al
	je	.L78
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L79
.L78:
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L80
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	xor	eax, 1
	test	al, al
	je	.L81
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L80
.L81:
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	xor	eax, 1
	test	al, al
	je	.L82
	movzx	eax, BYTE PTR a$r_buff1_thd3[rip]
	xor	eax, 1
	test	al, al
	je	.L82
.L80:
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L79
.L82:
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L84
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	test	al, al
	jne	.L85
.L84:
	mov	eax, 1
	jmp	.L86
.L85:
	mov	eax, 0
.L86:
	and	eax, 1
	test	al, al
	je	.L87
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L87
	mov	eax, 1
	jmp	.L79
.L87:
	mov	eax, 0
.L79:
	mov	BYTE PTR a$w_buff0_used[rip], al
	movzx	eax, BYTE PTR weak$$choice2[rip]
	test	al, al
	je	.L89
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L90
.L89:
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L91
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	xor	eax, 1
	test	al, al
	je	.L92
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L91
.L92:
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	xor	eax, 1
	test	al, al
	je	.L93
	movzx	eax, BYTE PTR a$r_buff1_thd3[rip]
	xor	eax, 1
	test	al, al
	je	.L93
.L91:
	mov	eax, 1
	jmp	.L94
.L93:
	mov	eax, 0
.L94:
	and	eax, 1
	test	al, al
	je	.L95
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L95
	mov	eax, 1
	jmp	.L90
.L95:
	mov	eax, 0
.L90:
	mov	BYTE PTR a$w_buff1_used[rip], al
	movzx	eax, BYTE PTR weak$$choice2[rip]
	test	al, al
	je	.L97
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L98
.L97:
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L99
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	xor	eax, 1
	test	al, al
	je	.L100
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L99
.L100:
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	xor	eax, 1
	test	al, al
	je	.L101
	movzx	eax, BYTE PTR a$r_buff1_thd3[rip]
	xor	eax, 1
	test	al, al
	je	.L101
.L99:
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L98
.L101:
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L103
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	test	al, al
	jne	.L104
.L103:
	mov	eax, 1
	jmp	.L105
.L104:
	mov	eax, 0
.L105:
	and	eax, 1
	test	al, al
	je	.L106
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	movzx	eax, al
	test	eax, eax
	je	.L106
	mov	eax, 1
	jmp	.L98
.L106:
	mov	eax, 0
.L98:
	mov	BYTE PTR a$r_buff0_thd3[rip], al
	movzx	eax, BYTE PTR weak$$choice2[rip]
	test	al, al
	je	.L108
	movzx	eax, BYTE PTR a$r_buff1_thd3[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L109
.L108:
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L110
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	xor	eax, 1
	test	al, al
	je	.L111
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L110
.L111:
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	xor	eax, 1
	test	al, al
	je	.L112
	movzx	eax, BYTE PTR a$r_buff1_thd3[rip]
	xor	eax, 1
	test	al, al
	je	.L112
.L110:
	mov	eax, 1
	jmp	.L113
.L112:
	mov	eax, 0
.L113:
	and	eax, 1
	test	al, al
	je	.L114
	movzx	eax, BYTE PTR a$r_buff1_thd3[rip]
	movzx	eax, al
	test	eax, eax
	je	.L114
	mov	eax, 1
	jmp	.L109
.L114:
	mov	eax, 0
.L109:
	mov	BYTE PTR a$r_buff1_thd3[rip], al
	mov	eax, DWORD PTR a[rip]
	mov	DWORD PTR __unbuffered_p2_EBX[rip], eax
	movzx	eax, BYTE PTR a$flush_delayed[rip]
	test	al, al
	je	.L116
	mov	eax, DWORD PTR a$mem_tmp[rip]
	jmp	.L117
.L116:
	mov	eax, DWORD PTR a[rip]
.L117:
	mov	DWORD PTR a[rip], eax
	mov	BYTE PTR a$flush_delayed[rip], 0
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L118
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	test	al, al
	jne	.L119
.L118:
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	test	al, al
	je	.L120
	movzx	eax, BYTE PTR a$r_buff1_thd3[rip]
	test	al, al
	je	.L120
	mov	eax, DWORD PTR a$w_buff1[rip]
	jmp	.L122
.L120:
	mov	eax, DWORD PTR a[rip]
	jmp	.L122
.L119:
	mov	eax, DWORD PTR a$w_buff0[rip]
.L122:
	mov	DWORD PTR a[rip], eax
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L123
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	test	al, al
	jne	.L124
.L123:
	mov	eax, 1
	jmp	.L125
.L124:
	mov	eax, 0
.L125:
	and	eax, 1
	test	al, al
	je	.L126
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L126
	mov	eax, 1
	jmp	.L127
.L126:
	mov	eax, 0
.L127:
	mov	BYTE PTR a$w_buff0_used[rip], al
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L128
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	test	al, al
	jne	.L129
.L128:
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	test	al, al
	je	.L130
	movzx	eax, BYTE PTR a$r_buff1_thd3[rip]
	test	al, al
	jne	.L129
.L130:
	mov	eax, 1
	jmp	.L131
.L129:
	mov	eax, 0
.L131:
	and	eax, 1
	test	al, al
	je	.L132
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L132
	mov	eax, 1
	jmp	.L133
.L132:
	mov	eax, 0
.L133:
	mov	BYTE PTR a$w_buff1_used[rip], al
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L134
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	test	al, al
	jne	.L135
.L134:
	mov	eax, 1
	jmp	.L136
.L135:
	mov	eax, 0
.L136:
	and	eax, 1
	test	al, al
	je	.L137
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	movzx	eax, al
	test	eax, eax
	je	.L137
	mov	eax, 1
	jmp	.L138
.L137:
	mov	eax, 0
.L138:
	mov	BYTE PTR a$r_buff0_thd3[rip], al
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L139
	movzx	eax, BYTE PTR a$r_buff0_thd3[rip]
	test	al, al
	jne	.L140
.L139:
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	test	al, al
	je	.L141
	movzx	eax, BYTE PTR a$r_buff1_thd3[rip]
	test	al, al
	jne	.L140
.L141:
	mov	eax, 1
	jmp	.L142
.L140:
	mov	eax, 0
.L142:
	and	eax, 1
	test	al, al
	je	.L143
	movzx	eax, BYTE PTR a$r_buff1_thd3[rip]
	movzx	eax, al
	test	eax, eax
	je	.L143
	mov	eax, 1
	jmp	.L144
.L143:
	mov	eax, 0
.L144:
	mov	BYTE PTR a$r_buff1_thd3[rip], al
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	mov	eax, DWORD PTR __unbuffered_cnt[rip]
	add	eax, 1
	mov	DWORD PTR __unbuffered_cnt[rip], eax
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	nondet_0@PLT
	cdqe
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE5:
	.size	P2, .-P2
	.globl	fence
	.type	fence, @function
fence:
.LFB6:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE6:
	.size	fence, .-fence
	.globl	isync
	.type	isync, @function
isync:
.LFB7:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE7:
	.size	isync, .-isync
	.globl	lwfence
	.type	lwfence, @function
lwfence:
.LFB8:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE8:
	.size	lwfence, .-lwfence
	.globl	main
	.type	main, @function
main:
.LFB9:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	mov	ecx, 0
	lea	rdx, P0[rip]
	mov	esi, 0
	mov	edi, 0
	call	pthread_create@PLT
	mov	ecx, 0
	lea	rdx, P1[rip]
	mov	esi, 0
	mov	edi, 0
	call	pthread_create@PLT
	mov	ecx, 0
	lea	rdx, P2[rip]
	mov	esi, 0
	mov	edi, 0
	call	pthread_create@PLT
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	mov	eax, DWORD PTR __unbuffered_cnt[rip]
	cmp	eax, 3
	sete	al
	mov	BYTE PTR main$tmp_guard0[rip], al
	mov	eax, 0
	call	__VERIFIER_atomic_end
	movzx	eax, BYTE PTR main$tmp_guard0[rip]
	movzx	eax, al
	mov	edi, eax
	mov	eax, 0
	call	__VERIFIER_assume@PLT
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L150
	movzx	eax, BYTE PTR a$r_buff0_thd0[rip]
	test	al, al
	jne	.L151
.L150:
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	test	al, al
	je	.L152
	movzx	eax, BYTE PTR a$r_buff1_thd0[rip]
	test	al, al
	je	.L152
	mov	eax, DWORD PTR a$w_buff1[rip]
	jmp	.L154
.L152:
	mov	eax, DWORD PTR a[rip]
	jmp	.L154
.L151:
	mov	eax, DWORD PTR a$w_buff0[rip]
.L154:
	mov	DWORD PTR a[rip], eax
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L155
	movzx	eax, BYTE PTR a$r_buff0_thd0[rip]
	test	al, al
	jne	.L156
.L155:
	mov	eax, 1
	jmp	.L157
.L156:
	mov	eax, 0
.L157:
	and	eax, 1
	test	al, al
	je	.L158
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L158
	mov	eax, 1
	jmp	.L159
.L158:
	mov	eax, 0
.L159:
	mov	BYTE PTR a$w_buff0_used[rip], al
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L160
	movzx	eax, BYTE PTR a$r_buff0_thd0[rip]
	test	al, al
	jne	.L161
.L160:
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	test	al, al
	je	.L162
	movzx	eax, BYTE PTR a$r_buff1_thd0[rip]
	test	al, al
	jne	.L161
.L162:
	mov	eax, 1
	jmp	.L163
.L161:
	mov	eax, 0
.L163:
	and	eax, 1
	test	al, al
	je	.L164
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L164
	mov	eax, 1
	jmp	.L165
.L164:
	mov	eax, 0
.L165:
	mov	BYTE PTR a$w_buff1_used[rip], al
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L166
	movzx	eax, BYTE PTR a$r_buff0_thd0[rip]
	test	al, al
	jne	.L167
.L166:
	mov	eax, 1
	jmp	.L168
.L167:
	mov	eax, 0
.L168:
	and	eax, 1
	test	al, al
	je	.L169
	movzx	eax, BYTE PTR a$r_buff0_thd0[rip]
	movzx	eax, al
	test	eax, eax
	je	.L169
	mov	eax, 1
	jmp	.L170
.L169:
	mov	eax, 0
.L170:
	mov	BYTE PTR a$r_buff0_thd0[rip], al
	movzx	eax, BYTE PTR a$w_buff0_used[rip]
	test	al, al
	je	.L171
	movzx	eax, BYTE PTR a$r_buff0_thd0[rip]
	test	al, al
	jne	.L172
.L171:
	movzx	eax, BYTE PTR a$w_buff1_used[rip]
	test	al, al
	je	.L173
	movzx	eax, BYTE PTR a$r_buff1_thd0[rip]
	test	al, al
	jne	.L172
.L173:
	mov	eax, 1
	jmp	.L174
.L172:
	mov	eax, 0
.L174:
	and	eax, 1
	test	al, al
	je	.L175
	movzx	eax, BYTE PTR a$r_buff1_thd0[rip]
	movzx	eax, al
	test	eax, eax
	je	.L175
	mov	eax, 1
	jmp	.L176
.L175:
	mov	eax, 0
.L176:
	mov	BYTE PTR a$r_buff1_thd0[rip], al
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	mov	eax, DWORD PTR __unbuffered_p0_EAX[rip]
	cmp	eax, 1
	jne	.L177
	mov	eax, DWORD PTR __unbuffered_p0_EBX[rip]
	test	eax, eax
	jne	.L177
	mov	eax, DWORD PTR __unbuffered_p1_EAX[rip]
	test	eax, eax
	jne	.L177
	mov	eax, DWORD PTR __unbuffered_p2_EAX[rip]
	cmp	eax, 1
	jne	.L177
	mov	eax, DWORD PTR __unbuffered_p2_EBX[rip]
	test	eax, eax
	je	.L178
.L177:
	mov	eax, 1
	jmp	.L179
.L178:
	mov	eax, 0
.L179:
	and	eax, 1
	mov	BYTE PTR main$tmp_guard1[rip], al
	mov	eax, 0
	call	__VERIFIER_atomic_end
	movzx	eax, BYTE PTR main$tmp_guard1[rip]
	movzx	eax, al
	mov	edi, eax
	call	__VERIFIER_assert
	mov	eax, 0
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE9:
	.size	main, .-main
	.ident	"GCC: (Ubuntu 10.5.0-1ubuntu1~20.04) 10.5.0"
	.section	.note.GNU-stack,"",@progbits
	.section	.note.gnu.property,"a"
	.align 8
	.long	 1f - 0f
	.long	 4f - 1f
	.long	 5
0:
	.string	 "GNU"
1:
	.align 8
	.long	 0xc0000002
	.long	 3f - 2f
2:
	.long	 0x3
3:
	.align 8
4:

	.arch armv5t
	.eabi_attribute 20, 1
	.eabi_attribute 21, 1
	.eabi_attribute 23, 3
	.eabi_attribute 24, 1
	.eabi_attribute 25, 1
	.eabi_attribute 26, 2
	.eabi_attribute 30, 6
	.eabi_attribute 34, 0
	.eabi_attribute 18, 4
	.file	"342819.c"
	.text
	.align	2
	.global	__VERIFIER_assert
	.syntax unified
	.arm
	.fpu softvfp
	.type	__VERIFIER_assert, %function
__VERIFIER_assert:
	@ args = 0, pretend = 0, frame = 8
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #8
	str	r0, [fp, #-8]
	ldr	r3, [fp, #-8]
	cmp	r3, #0
	bne	.L5
	nop
.L3:
	bl	__VERIFIER_error
.L5:
	nop
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
	.size	__VERIFIER_assert, .-__VERIFIER_assert
	.comm	__global_lock,4,4
	.align	2
	.global	__VERIFIER_atomic_begin
	.syntax unified
	.arm
	.fpu softvfp
	.type	__VERIFIER_atomic_begin, %function
__VERIFIER_atomic_begin:
	@ args = 0, pretend = 0, frame = 0
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	ldr	r3, .L8
	ldr	r3, [r3]
	cmp	r3, #0
	moveq	r3, #1
	movne	r3, #0
	and	r3, r3, #255
	mov	r0, r3
	bl	__VERIFIER_assume
	ldr	r3, .L8
	mov	r2, #1
	str	r2, [r3]
	nop
	pop	{fp, pc}
.L9:
	.align	2
.L8:
	.word	__global_lock
	.size	__VERIFIER_atomic_begin, .-__VERIFIER_atomic_begin
	.align	2
	.global	__VERIFIER_atomic_end
	.syntax unified
	.arm
	.fpu softvfp
	.type	__VERIFIER_atomic_end, %function
__VERIFIER_atomic_end:
	@ args = 0, pretend = 0, frame = 0
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	ldr	r3, .L12
	ldr	r3, [r3]
	cmp	r3, #1
	moveq	r3, #1
	movne	r3, #0
	and	r3, r3, #255
	mov	r0, r3
	bl	__VERIFIER_assume
	ldr	r3, .L12
	mov	r2, #0
	str	r2, [r3]
	nop
	pop	{fp, pc}
.L13:
	.align	2
.L12:
	.word	__global_lock
	.size	__VERIFIER_atomic_end, .-__VERIFIER_atomic_end
	.global	__unbuffered_cnt
	.bss
	.align	2
	.type	__unbuffered_cnt, %object
	.size	__unbuffered_cnt, 4
__unbuffered_cnt:
	.space	4
	.global	__unbuffered_p0_EAX
	.align	2
	.type	__unbuffered_p0_EAX, %object
	.size	__unbuffered_p0_EAX, 4
__unbuffered_p0_EAX:
	.space	4
	.global	__unbuffered_p0_EBX
	.align	2
	.type	__unbuffered_p0_EBX, %object
	.size	__unbuffered_p0_EBX, 4
__unbuffered_p0_EBX:
	.space	4
	.global	__unbuffered_p1_EAX
	.align	2
	.type	__unbuffered_p1_EAX, %object
	.size	__unbuffered_p1_EAX, 4
__unbuffered_p1_EAX:
	.space	4
	.global	__unbuffered_p2_EAX
	.align	2
	.type	__unbuffered_p2_EAX, %object
	.size	__unbuffered_p2_EAX, 4
__unbuffered_p2_EAX:
	.space	4
	.global	__unbuffered_p2_EBX
	.align	2
	.type	__unbuffered_p2_EBX, %object
	.size	__unbuffered_p2_EBX, 4
__unbuffered_p2_EBX:
	.space	4
	.global	a
	.align	2
	.type	a, %object
	.size	a, 4
a:
	.space	4
	.comm	a$flush_delayed,1,1
	.comm	a$mem_tmp,4,4
	.comm	a$r_buff0_thd0,1,1
	.comm	a$r_buff0_thd1,1,1
	.comm	a$r_buff0_thd2,1,1
	.comm	a$r_buff0_thd3,1,1
	.comm	a$r_buff1_thd0,1,1
	.comm	a$r_buff1_thd1,1,1
	.comm	a$r_buff1_thd2,1,1
	.comm	a$r_buff1_thd3,1,1
	.comm	a$read_delayed,1,1
	.comm	a$read_delayed_var,4,4
	.comm	a$w_buff0,4,4
	.comm	a$w_buff0_used,1,1
	.comm	a$w_buff1,4,4
	.comm	a$w_buff1_used,1,1
	.comm	main$tmp_guard0,1,1
	.comm	main$tmp_guard1,1,1
	.global	x
	.align	2
	.type	x, %object
	.size	x, 4
x:
	.space	4
	.global	y
	.align	2
	.type	y, %object
	.size	y, 4
y:
	.space	4
	.global	z
	.align	2
	.type	z, %object
	.size	z, 4
z:
	.space	4
	.comm	weak$$choice0,1,1
	.comm	weak$$choice2,1,1
	.text
	.align	2
	.global	P0
	.syntax unified
	.arm
	.fpu softvfp
	.type	P0, %function
P0:
	@ args = 0, pretend = 0, frame = 8
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #8
	str	r0, [fp, #-8]
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L46
	ldr	r3, [r3]
	ldr	r2, .L46+4
	str	r3, [r2]
	ldr	r3, .L46
	mov	r2, #1
	str	r2, [r3]
	ldr	r3, .L46+8
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L46+12
	strb	r2, [r3]
	ldr	r3, .L46+8
	mov	r2, #1
	strb	r2, [r3]
	ldr	r3, .L46+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L15
	ldr	r3, .L46+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L16
.L15:
	mov	r3, #1
	b	.L17
.L16:
	mov	r3, #0
.L17:
	mov	r0, r3
	bl	__VERIFIER_assert
	ldr	r3, .L46+16
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L46+20
	strb	r2, [r3]
	ldr	r3, .L46+24
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L46+28
	strb	r2, [r3]
	ldr	r3, .L46+32
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L46+36
	strb	r2, [r3]
	ldr	r3, .L46+40
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L46+44
	strb	r2, [r3]
	ldr	r3, .L46+24
	mov	r2, #1
	strb	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L46+48
	mov	r2, #1
	str	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L46+48
	ldr	r3, [r3]
	ldr	r2, .L46+52
	str	r3, [r2]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L46+56
	ldr	r3, [r3]
	ldr	r2, .L46+60
	str	r3, [r2]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L46+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L18
	ldr	r3, .L46+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L19
.L18:
	ldr	r3, .L46+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L20
	ldr	r3, .L46+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L20
	ldr	r3, .L46+4
	ldr	r3, [r3]
	b	.L22
.L20:
	ldr	r3, .L46+64
	ldr	r3, [r3]
	b	.L22
.L19:
	ldr	r3, .L46
	ldr	r3, [r3]
.L22:
	ldr	r2, .L46+64
	str	r3, [r2]
	ldr	r3, .L46+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L23
	ldr	r3, .L46+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L24
.L23:
	mov	r3, #1
	b	.L25
.L24:
	mov	r3, #0
.L25:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L26
	ldr	r3, .L46+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L26
	mov	r2, #1
	b	.L27
.L26:
	mov	r2, #0
.L27:
	ldr	r3, .L46+8
	strb	r2, [r3]
	ldr	r3, .L46+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L28
	ldr	r3, .L46+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L29
.L28:
	ldr	r3, .L46+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L30
	ldr	r3, .L46+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L29
.L30:
	mov	r3, #1
	b	.L31
.L29:
	mov	r3, #0
.L31:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L32
	ldr	r3, .L46+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L32
	mov	r2, #1
	b	.L33
.L32:
	mov	r2, #0
.L33:
	ldr	r3, .L46+12
	strb	r2, [r3]
	ldr	r3, .L46+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L34
	ldr	r3, .L46+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L35
.L34:
	mov	r3, #1
	b	.L36
.L35:
	mov	r3, #0
.L36:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L37
	ldr	r3, .L46+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L37
	mov	r2, #1
	b	.L38
.L37:
	mov	r2, #0
.L38:
	ldr	r3, .L46+24
	strb	r2, [r3]
	ldr	r3, .L46+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L39
	ldr	r3, .L46+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L40
.L39:
	ldr	r3, .L46+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L41
	ldr	r3, .L46+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L40
.L41:
	mov	r3, #1
	b	.L42
.L40:
	mov	r3, #0
.L42:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L43
	ldr	r3, .L46+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L43
	mov	r2, #1
	b	.L44
.L43:
	mov	r2, #0
.L44:
	ldr	r3, .L46+28
	strb	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L46+68
	ldr	r3, [r3]
	add	r3, r3, #1
	ldr	r2, .L46+68
	str	r3, [r2]
	bl	__VERIFIER_atomic_end
	bl	nondet_0
	mov	r3, r0
	mov	r0, r3
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
.L47:
	.align	2
.L46:
	.word	a$w_buff0
	.word	a$w_buff1
	.word	a$w_buff0_used
	.word	a$w_buff1_used
	.word	a$r_buff0_thd0
	.word	a$r_buff1_thd0
	.word	a$r_buff0_thd1
	.word	a$r_buff1_thd1
	.word	a$r_buff0_thd2
	.word	a$r_buff1_thd2
	.word	a$r_buff0_thd3
	.word	a$r_buff1_thd3
	.word	x
	.word	__unbuffered_p0_EAX
	.word	y
	.word	__unbuffered_p0_EBX
	.word	a
	.word	__unbuffered_cnt
	.size	P0, .-P0
	.align	2
	.global	P1
	.syntax unified
	.arm
	.fpu softvfp
	.type	P1, %function
P1:
	@ args = 0, pretend = 0, frame = 8
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #8
	str	r0, [fp, #-8]
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L77
	mov	r2, #1
	str	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L77+4
	ldr	r3, [r3]
	ldr	r2, .L77+8
	str	r3, [r2]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L77+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L49
	ldr	r3, .L77+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L50
.L49:
	ldr	r3, .L77+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L51
	ldr	r3, .L77+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L51
	ldr	r3, .L77+28
	ldr	r3, [r3]
	b	.L53
.L51:
	ldr	r3, .L77+32
	ldr	r3, [r3]
	b	.L53
.L50:
	ldr	r3, .L77+36
	ldr	r3, [r3]
.L53:
	ldr	r2, .L77+32
	str	r3, [r2]
	ldr	r3, .L77+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L54
	ldr	r3, .L77+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L55
.L54:
	mov	r3, #1
	b	.L56
.L55:
	mov	r3, #0
.L56:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L57
	ldr	r3, .L77+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L57
	mov	r2, #1
	b	.L58
.L57:
	mov	r2, #0
.L58:
	ldr	r3, .L77+12
	strb	r2, [r3]
	ldr	r3, .L77+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L59
	ldr	r3, .L77+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L60
.L59:
	ldr	r3, .L77+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L61
	ldr	r3, .L77+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L60
.L61:
	mov	r3, #1
	b	.L62
.L60:
	mov	r3, #0
.L62:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L63
	ldr	r3, .L77+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L63
	mov	r2, #1
	b	.L64
.L63:
	mov	r2, #0
.L64:
	ldr	r3, .L77+20
	strb	r2, [r3]
	ldr	r3, .L77+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L65
	ldr	r3, .L77+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L66
.L65:
	mov	r3, #1
	b	.L67
.L66:
	mov	r3, #0
.L67:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L68
	ldr	r3, .L77+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L68
	mov	r2, #1
	b	.L69
.L68:
	mov	r2, #0
.L69:
	ldr	r3, .L77+16
	strb	r2, [r3]
	ldr	r3, .L77+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L70
	ldr	r3, .L77+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L71
.L70:
	ldr	r3, .L77+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L72
	ldr	r3, .L77+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L71
.L72:
	mov	r3, #1
	b	.L73
.L71:
	mov	r3, #0
.L73:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L74
	ldr	r3, .L77+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L74
	mov	r2, #1
	b	.L75
.L74:
	mov	r2, #0
.L75:
	ldr	r3, .L77+24
	strb	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L77+40
	ldr	r3, [r3]
	add	r3, r3, #1
	ldr	r2, .L77+40
	str	r3, [r2]
	bl	__VERIFIER_atomic_end
	bl	nondet_0
	mov	r3, r0
	mov	r0, r3
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
.L78:
	.align	2
.L77:
	.word	y
	.word	z
	.word	__unbuffered_p1_EAX
	.word	a$w_buff0_used
	.word	a$r_buff0_thd2
	.word	a$w_buff1_used
	.word	a$r_buff1_thd2
	.word	a$w_buff1
	.word	a
	.word	a$w_buff0
	.word	__unbuffered_cnt
	.size	P1, .-P1
	.align	2
	.global	P2
	.syntax unified
	.arm
	.fpu softvfp
	.type	P2, %function
P2:
	@ args = 0, pretend = 0, frame = 8
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #8
	str	r0, [fp, #-8]
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L154
	mov	r2, #1
	str	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L154
	ldr	r3, [r3]
	ldr	r2, .L154+4
	str	r3, [r2]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	bl	nondet_1
	mov	r3, r0
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r2, r3, #255
	ldr	r3, .L154+8
	strb	r2, [r3]
	bl	nondet_1
	mov	r3, r0
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r2, r3, #255
	ldr	r3, .L154+12
	strb	r2, [r3]
	ldr	r3, .L154+12
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L154+16
	strb	r2, [r3]
	ldr	r3, .L154+20
	ldr	r3, [r3]
	ldr	r2, .L154+24
	str	r3, [r2]
	ldr	r3, .L154+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L80
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L81
	ldr	r3, .L154+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L80
.L81:
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L82
	ldr	r3, .L154+40
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L80
.L82:
	ldr	r3, .L154+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L83
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L83
	ldr	r3, .L154+44
	ldr	r3, [r3]
	b	.L85
.L83:
	ldr	r3, .L154+48
	ldr	r3, [r3]
	b	.L85
.L80:
	ldr	r3, .L154+20
	ldr	r3, [r3]
.L85:
	ldr	r2, .L154+20
	str	r3, [r2]
	ldr	r3, .L154+44
	ldr	r3, [r3]
	ldr	r2, .L154+44
	str	r3, [r2]
	ldr	r3, .L154+48
	ldr	r3, [r3]
	ldr	r2, .L154+48
	str	r3, [r2]
	ldr	r3, .L154+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L86
	ldr	r3, .L154+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L87
.L86:
	ldr	r3, .L154+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L88
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L89
	ldr	r3, .L154+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L88
.L89:
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L90
	ldr	r3, .L154+40
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L90
.L88:
	ldr	r3, .L154+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L87
.L90:
	ldr	r3, .L154+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L92
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L93
.L92:
	mov	r3, #1
	b	.L94
.L93:
	mov	r3, #0
.L94:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L95
	ldr	r3, .L154+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L95
	mov	r3, #1
	b	.L87
.L95:
	mov	r3, #0
.L87:
	ldr	r2, .L154+28
	strb	r3, [r2]
	ldr	r3, .L154+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L97
	ldr	r3, .L154+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L98
.L97:
	ldr	r3, .L154+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L99
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L100
	ldr	r3, .L154+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L99
.L100:
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L101
	ldr	r3, .L154+40
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L101
.L99:
	mov	r3, #1
	b	.L102
.L101:
	mov	r3, #0
.L102:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L103
	ldr	r3, .L154+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L103
	mov	r3, #1
	b	.L98
.L103:
	mov	r3, #0
.L98:
	ldr	r2, .L154+36
	strb	r3, [r2]
	ldr	r3, .L154+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L105
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L106
.L105:
	ldr	r3, .L154+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L107
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L108
	ldr	r3, .L154+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L107
.L108:
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L109
	ldr	r3, .L154+40
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L109
.L107:
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L106
.L109:
	ldr	r3, .L154+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L111
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L112
.L111:
	mov	r3, #1
	b	.L113
.L112:
	mov	r3, #0
.L113:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L114
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L114
	mov	r3, #1
	b	.L106
.L114:
	mov	r3, #0
.L106:
	ldr	r2, .L154+32
	strb	r3, [r2]
	ldr	r3, .L154+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L116
	ldr	r3, .L154+40
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L117
.L116:
	ldr	r3, .L154+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L118
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L119
	ldr	r3, .L154+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L118
.L119:
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L120
	ldr	r3, .L154+40
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L120
.L118:
	mov	r3, #1
	b	.L121
.L120:
	mov	r3, #0
.L121:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L122
	ldr	r3, .L154+40
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L122
	mov	r3, #1
	b	.L117
.L122:
	mov	r3, #0
.L117:
	ldr	r2, .L154+40
	strb	r3, [r2]
	ldr	r3, .L154+20
	ldr	r3, [r3]
	ldr	r2, .L154+52
	str	r3, [r2]
	ldr	r3, .L154+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L124
	ldr	r3, .L154+24
	ldr	r3, [r3]
	b	.L125
.L124:
	ldr	r3, .L154+20
	ldr	r3, [r3]
.L125:
	ldr	r2, .L154+20
	str	r3, [r2]
	ldr	r3, .L154+16
	mov	r2, #0
	strb	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L154+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L126
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L127
.L126:
	ldr	r3, .L154+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L128
	ldr	r3, .L154+40
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L128
	ldr	r3, .L154+48
	ldr	r3, [r3]
	b	.L130
.L128:
	ldr	r3, .L154+20
	ldr	r3, [r3]
	b	.L130
.L127:
	ldr	r3, .L154+44
	ldr	r3, [r3]
.L130:
	ldr	r2, .L154+20
	str	r3, [r2]
	ldr	r3, .L154+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L131
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L132
.L131:
	mov	r3, #1
	b	.L133
.L132:
	mov	r3, #0
.L133:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L134
	ldr	r3, .L154+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L134
	mov	r2, #1
	b	.L135
.L134:
	mov	r2, #0
.L135:
	ldr	r3, .L154+28
	strb	r2, [r3]
	ldr	r3, .L154+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L136
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L137
.L136:
	ldr	r3, .L154+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L138
	ldr	r3, .L154+40
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L137
.L138:
	mov	r3, #1
	b	.L139
.L137:
	mov	r3, #0
.L139:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L140
	ldr	r3, .L154+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L140
	mov	r2, #1
	b	.L141
.L140:
	mov	r2, #0
.L141:
	ldr	r3, .L154+36
	strb	r2, [r3]
	ldr	r3, .L154+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L142
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L143
.L142:
	mov	r3, #1
	b	.L144
.L143:
	mov	r3, #0
.L144:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L145
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L145
	mov	r2, #1
	b	.L146
.L145:
	mov	r2, #0
.L146:
	ldr	r3, .L154+32
	strb	r2, [r3]
	ldr	r3, .L154+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L147
	ldr	r3, .L154+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L148
.L147:
	ldr	r3, .L154+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L149
	ldr	r3, .L154+40
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L148
.L149:
	mov	r3, #1
	b	.L150
.L148:
	mov	r3, #0
.L150:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L151
	ldr	r3, .L154+40
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L151
	mov	r2, #1
	b	.L152
.L151:
	mov	r2, #0
.L152:
	ldr	r3, .L154+40
	strb	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L154+56
	ldr	r3, [r3]
	add	r3, r3, #1
	ldr	r2, .L154+56
	str	r3, [r2]
	bl	__VERIFIER_atomic_end
	bl	nondet_0
	mov	r3, r0
	mov	r0, r3
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
.L155:
	.align	2
.L154:
	.word	z
	.word	__unbuffered_p2_EAX
	.word	weak$$choice0
	.word	weak$$choice2
	.word	a$flush_delayed
	.word	a
	.word	a$mem_tmp
	.word	a$w_buff0_used
	.word	a$r_buff0_thd3
	.word	a$w_buff1_used
	.word	a$r_buff1_thd3
	.word	a$w_buff0
	.word	a$w_buff1
	.word	__unbuffered_p2_EBX
	.word	__unbuffered_cnt
	.size	P2, .-P2
	.align	2
	.global	fence
	.syntax unified
	.arm
	.fpu softvfp
	.type	fence, %function
fence:
	@ args = 0, pretend = 0, frame = 0
	@ frame_needed = 1, uses_anonymous_args = 0
	@ link register save eliminated.
	str	fp, [sp, #-4]!
	add	fp, sp, #0
	nop
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
	.size	fence, .-fence
	.align	2
	.global	isync
	.syntax unified
	.arm
	.fpu softvfp
	.type	isync, %function
isync:
	@ args = 0, pretend = 0, frame = 0
	@ frame_needed = 1, uses_anonymous_args = 0
	@ link register save eliminated.
	str	fp, [sp, #-4]!
	add	fp, sp, #0
	nop
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
	.size	isync, .-isync
	.align	2
	.global	lwfence
	.syntax unified
	.arm
	.fpu softvfp
	.type	lwfence, %function
lwfence:
	@ args = 0, pretend = 0, frame = 0
	@ frame_needed = 1, uses_anonymous_args = 0
	@ link register save eliminated.
	str	fp, [sp, #-4]!
	add	fp, sp, #0
	nop
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
	.size	lwfence, .-lwfence
	.align	2
	.global	main
	.syntax unified
	.arm
	.fpu softvfp
	.type	main, %function
main:
	@ args = 0, pretend = 0, frame = 0
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	mov	r3, #0
	ldr	r2, .L191
	mov	r1, #0
	mov	r0, #0
	bl	pthread_create
	mov	r3, #0
	ldr	r2, .L191+4
	mov	r1, #0
	mov	r0, #0
	bl	pthread_create
	mov	r3, #0
	ldr	r2, .L191+8
	mov	r1, #0
	mov	r0, #0
	bl	pthread_create
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L191+12
	ldr	r3, [r3]
	cmp	r3, #3
	moveq	r3, #1
	movne	r3, #0
	and	r2, r3, #255
	ldr	r3, .L191+16
	strb	r2, [r3]
	bl	__VERIFIER_atomic_end
	ldr	r3, .L191+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	mov	r0, r3
	bl	__VERIFIER_assume
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L191+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L160
	ldr	r3, .L191+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L161
.L160:
	ldr	r3, .L191+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L162
	ldr	r3, .L191+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L162
	ldr	r3, .L191+36
	ldr	r3, [r3]
	b	.L164
.L162:
	ldr	r3, .L191+40
	ldr	r3, [r3]
	b	.L164
.L161:
	ldr	r3, .L191+44
	ldr	r3, [r3]
.L164:
	ldr	r2, .L191+40
	str	r3, [r2]
	ldr	r3, .L191+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L165
	ldr	r3, .L191+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L166
.L165:
	mov	r3, #1
	b	.L167
.L166:
	mov	r3, #0
.L167:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L168
	ldr	r3, .L191+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L168
	mov	r2, #1
	b	.L169
.L168:
	mov	r2, #0
.L169:
	ldr	r3, .L191+20
	strb	r2, [r3]
	ldr	r3, .L191+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L170
	ldr	r3, .L191+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L171
.L170:
	ldr	r3, .L191+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L172
	ldr	r3, .L191+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L171
.L172:
	mov	r3, #1
	b	.L173
.L171:
	mov	r3, #0
.L173:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L174
	ldr	r3, .L191+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L174
	mov	r2, #1
	b	.L175
.L174:
	mov	r2, #0
.L175:
	ldr	r3, .L191+28
	strb	r2, [r3]
	ldr	r3, .L191+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L176
	ldr	r3, .L191+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L177
.L176:
	mov	r3, #1
	b	.L178
.L177:
	mov	r3, #0
.L178:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L179
	ldr	r3, .L191+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L179
	mov	r2, #1
	b	.L180
.L179:
	mov	r2, #0
.L180:
	ldr	r3, .L191+24
	strb	r2, [r3]
	ldr	r3, .L191+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L181
	ldr	r3, .L191+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L182
.L181:
	ldr	r3, .L191+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L183
	ldr	r3, .L191+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L182
.L183:
	mov	r3, #1
	b	.L184
.L182:
	mov	r3, #0
.L184:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L185
	ldr	r3, .L191+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L185
	mov	r2, #1
	b	.L186
.L185:
	mov	r2, #0
.L186:
	ldr	r3, .L191+32
	strb	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L191+48
	ldr	r3, [r3]
	cmp	r3, #1
	bne	.L187
	ldr	r3, .L191+52
	ldr	r3, [r3]
	cmp	r3, #0
	bne	.L187
	ldr	r3, .L191+56
	ldr	r3, [r3]
	cmp	r3, #0
	bne	.L187
	ldr	r3, .L191+60
	ldr	r3, [r3]
	cmp	r3, #1
	bne	.L187
	ldr	r3, .L191+64
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L188
.L187:
	mov	r3, #1
	b	.L189
.L188:
	mov	r3, #0
.L189:
	and	r3, r3, #1
	and	r2, r3, #255
	ldr	r3, .L191+68
	strb	r2, [r3]
	bl	__VERIFIER_atomic_end
	ldr	r3, .L191+68
	ldrb	r3, [r3]	@ zero_extendqisi2
	mov	r0, r3
	bl	__VERIFIER_assert
	mov	r3, #0
	mov	r0, r3
	pop	{fp, pc}
.L192:
	.align	2
.L191:
	.word	P0
	.word	P1
	.word	P2
	.word	__unbuffered_cnt
	.word	main$tmp_guard0
	.word	a$w_buff0_used
	.word	a$r_buff0_thd0
	.word	a$w_buff1_used
	.word	a$r_buff1_thd0
	.word	a$w_buff1
	.word	a
	.word	a$w_buff0
	.word	__unbuffered_p0_EAX
	.word	__unbuffered_p0_EBX
	.word	__unbuffered_p1_EAX
	.word	__unbuffered_p2_EAX
	.word	__unbuffered_p2_EBX
	.word	main$tmp_guard1
	.size	main, .-main
	.ident	"GCC: (Ubuntu 9.4.0-1ubuntu1~20.04.2) 9.4.0"
	.section	.note.GNU-stack,"",%progbits
