	.file	"1257268.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_p1_EAX
	.align 4
	.type	__unbuffered_p1_EAX, @object
	.size	__unbuffered_p1_EAX, 4
__unbuffered_p1_EAX:
	.zero	4
	.globl	__unbuffered_p1_EBX
	.align 4
	.type	__unbuffered_p1_EBX, @object
	.size	__unbuffered_p1_EBX, 4
__unbuffered_p1_EBX:
	.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_p3_EAX
	.align 4
	.type	__unbuffered_p3_EAX, @object
	.size	__unbuffered_p3_EAX, 4
__unbuffered_p3_EAX:
	.zero	4
	.globl	__unbuffered_p3_EBX
	.align 4
	.type	__unbuffered_p3_EBX, @object
	.size	__unbuffered_p3_EBX, 4
__unbuffered_p3_EBX:
	.zero	4
	.globl	a
	.align 4
	.type	a, @object
	.size	a, 4
a:
	.zero	4
	.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	x$flush_delayed
	.type	x$flush_delayed, @object
	.size	x$flush_delayed, 1
x$flush_delayed:
	.zero	1
	.globl	x$mem_tmp
	.align 4
	.type	x$mem_tmp, @object
	.size	x$mem_tmp, 4
x$mem_tmp:
	.zero	4
	.globl	x$r_buff0_thd0
	.type	x$r_buff0_thd0, @object
	.size	x$r_buff0_thd0, 1
x$r_buff0_thd0:
	.zero	1
	.globl	x$r_buff0_thd1
	.type	x$r_buff0_thd1, @object
	.size	x$r_buff0_thd1, 1
x$r_buff0_thd1:
	.zero	1
	.globl	x$r_buff0_thd2
	.type	x$r_buff0_thd2, @object
	.size	x$r_buff0_thd2, 1
x$r_buff0_thd2:
	.zero	1
	.globl	x$r_buff0_thd3
	.type	x$r_buff0_thd3, @object
	.size	x$r_buff0_thd3, 1
x$r_buff0_thd3:
	.zero	1
	.globl	x$r_buff0_thd4
	.type	x$r_buff0_thd4, @object
	.size	x$r_buff0_thd4, 1
x$r_buff0_thd4:
	.zero	1
	.globl	x$r_buff1_thd0
	.type	x$r_buff1_thd0, @object
	.size	x$r_buff1_thd0, 1
x$r_buff1_thd0:
	.zero	1
	.globl	x$r_buff1_thd1
	.type	x$r_buff1_thd1, @object
	.size	x$r_buff1_thd1, 1
x$r_buff1_thd1:
	.zero	1
	.globl	x$r_buff1_thd2
	.type	x$r_buff1_thd2, @object
	.size	x$r_buff1_thd2, 1
x$r_buff1_thd2:
	.zero	1
	.globl	x$r_buff1_thd3
	.type	x$r_buff1_thd3, @object
	.size	x$r_buff1_thd3, 1
x$r_buff1_thd3:
	.zero	1
	.globl	x$r_buff1_thd4
	.type	x$r_buff1_thd4, @object
	.size	x$r_buff1_thd4, 1
x$r_buff1_thd4:
	.zero	1
	.globl	x$read_delayed
	.type	x$read_delayed, @object
	.size	x$read_delayed, 1
x$read_delayed:
	.zero	1
	.globl	x$read_delayed_var
	.align 8
	.type	x$read_delayed_var, @object
	.size	x$read_delayed_var, 8
x$read_delayed_var:
	.zero	8
	.globl	x$w_buff0
	.align 4
	.type	x$w_buff0, @object
	.size	x$w_buff0, 4
x$w_buff0:
	.zero	4
	.globl	x$w_buff0_used
	.type	x$w_buff0_used, @object
	.size	x$w_buff0_used, 1
x$w_buff0_used:
	.zero	1
	.globl	x$w_buff1
	.align 4
	.type	x$w_buff1, @object
	.size	x$w_buff1, 4
x$w_buff1:
	.zero	4
	.globl	x$w_buff1_used
	.type	x$w_buff1_used, @object
	.size	x$w_buff1_used, 1
x$w_buff1_used:
	.zero	1
	.globl	y
	.align 4
	.type	y, @object
	.size	y, 4
y:
	.zero	4
	.globl	y$flush_delayed
	.type	y$flush_delayed, @object
	.size	y$flush_delayed, 1
y$flush_delayed:
	.zero	1
	.globl	y$mem_tmp
	.align 4
	.type	y$mem_tmp, @object
	.size	y$mem_tmp, 4
y$mem_tmp:
	.zero	4
	.globl	y$r_buff0_thd0
	.type	y$r_buff0_thd0, @object
	.size	y$r_buff0_thd0, 1
y$r_buff0_thd0:
	.zero	1
	.globl	y$r_buff0_thd1
	.type	y$r_buff0_thd1, @object
	.size	y$r_buff0_thd1, 1
y$r_buff0_thd1:
	.zero	1
	.globl	y$r_buff0_thd2
	.type	y$r_buff0_thd2, @object
	.size	y$r_buff0_thd2, 1
y$r_buff0_thd2:
	.zero	1
	.globl	y$r_buff0_thd3
	.type	y$r_buff0_thd3, @object
	.size	y$r_buff0_thd3, 1
y$r_buff0_thd3:
	.zero	1
	.globl	y$r_buff0_thd4
	.type	y$r_buff0_thd4, @object
	.size	y$r_buff0_thd4, 1
y$r_buff0_thd4:
	.zero	1
	.globl	y$r_buff1_thd0
	.type	y$r_buff1_thd0, @object
	.size	y$r_buff1_thd0, 1
y$r_buff1_thd0:
	.zero	1
	.globl	y$r_buff1_thd1
	.type	y$r_buff1_thd1, @object
	.size	y$r_buff1_thd1, 1
y$r_buff1_thd1:
	.zero	1
	.globl	y$r_buff1_thd2
	.type	y$r_buff1_thd2, @object
	.size	y$r_buff1_thd2, 1
y$r_buff1_thd2:
	.zero	1
	.globl	y$r_buff1_thd3
	.type	y$r_buff1_thd3, @object
	.size	y$r_buff1_thd3, 1
y$r_buff1_thd3:
	.zero	1
	.globl	y$r_buff1_thd4
	.type	y$r_buff1_thd4, @object
	.size	y$r_buff1_thd4, 1
y$r_buff1_thd4:
	.zero	1
	.globl	y$read_delayed
	.type	y$read_delayed, @object
	.size	y$read_delayed, 1
y$read_delayed:
	.zero	1
	.globl	y$read_delayed_var
	.align 8
	.type	y$read_delayed_var, @object
	.size	y$read_delayed_var, 8
y$read_delayed_var:
	.zero	8
	.globl	y$w_buff0
	.align 4
	.type	y$w_buff0, @object
	.size	y$w_buff0, 4
y$w_buff0:
	.zero	4
	.globl	y$w_buff0_used
	.type	y$w_buff0_used, @object
	.size	y$w_buff0_used, 1
y$w_buff0_used:
	.zero	1
	.globl	y$w_buff1
	.align 4
	.type	y$w_buff1, @object
	.size	y$w_buff1, 4
y$w_buff1:
	.zero	4
	.globl	y$w_buff1_used
	.type	y$w_buff1_used, @object
	.size	y$w_buff1_used, 1
y$w_buff1_used:
	.zero	1
	.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	DWORD PTR a[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
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L11
	movzx	eax, BYTE PTR x$r_buff0_thd1[rip]
	test	al, al
	jne	.L12
.L11:
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	test	al, al
	je	.L13
	movzx	eax, BYTE PTR x$r_buff1_thd1[rip]
	test	al, al
	je	.L13
	mov	eax, DWORD PTR x$w_buff1[rip]
	jmp	.L15
.L13:
	mov	eax, DWORD PTR x[rip]
	jmp	.L15
.L12:
	mov	eax, DWORD PTR x$w_buff0[rip]
.L15:
	mov	DWORD PTR x[rip], eax
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L16
	movzx	eax, BYTE PTR x$r_buff0_thd1[rip]
	test	al, al
	jne	.L17
.L16:
	mov	eax, 1
	jmp	.L18
.L17:
	mov	eax, 0
.L18:
	and	eax, 1
	test	al, al
	je	.L19
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L19
	mov	eax, 1
	jmp	.L20
.L19:
	mov	eax, 0
.L20:
	mov	BYTE PTR x$w_buff0_used[rip], al
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L21
	movzx	eax, BYTE PTR x$r_buff0_thd1[rip]
	test	al, al
	jne	.L22
.L21:
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	test	al, al
	je	.L23
	movzx	eax, BYTE PTR x$r_buff1_thd1[rip]
	test	al, al
	jne	.L22
.L23:
	mov	eax, 1
	jmp	.L24
.L22:
	mov	eax, 0
.L24:
	and	eax, 1
	test	al, al
	je	.L25
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L25
	mov	eax, 1
	jmp	.L26
.L25:
	mov	eax, 0
.L26:
	mov	BYTE PTR x$w_buff1_used[rip], al
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L27
	movzx	eax, BYTE PTR x$r_buff0_thd1[rip]
	test	al, al
	jne	.L28
.L27:
	mov	eax, 1
	jmp	.L29
.L28:
	mov	eax, 0
.L29:
	and	eax, 1
	test	al, al
	je	.L30
	movzx	eax, BYTE PTR x$r_buff0_thd1[rip]
	movzx	eax, al
	test	eax, eax
	je	.L30
	mov	eax, 1
	jmp	.L31
.L30:
	mov	eax, 0
.L31:
	mov	BYTE PTR x$r_buff0_thd1[rip], al
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L32
	movzx	eax, BYTE PTR x$r_buff0_thd1[rip]
	test	al, al
	jne	.L33
.L32:
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	test	al, al
	je	.L34
	movzx	eax, BYTE PTR x$r_buff1_thd1[rip]
	test	al, al
	jne	.L33
.L34:
	mov	eax, 1
	jmp	.L35
.L33:
	mov	eax, 0
.L35:
	and	eax, 1
	test	al, al
	je	.L36
	movzx	eax, BYTE PTR x$r_buff1_thd1[rip]
	movzx	eax, al
	test	eax, eax
	je	.L36
	mov	eax, 1
	jmp	.L37
.L36:
	mov	eax, 0
.L37:
	mov	BYTE PTR x$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	eax, DWORD PTR x$w_buff0[rip]
	mov	DWORD PTR x$w_buff1[rip], eax
	mov	DWORD PTR x$w_buff0[rip], 2
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	mov	BYTE PTR x$w_buff1_used[rip], al
	mov	BYTE PTR x$w_buff0_used[rip], 1
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L40
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	je	.L41
.L40:
	mov	eax, 1
	jmp	.L42
.L41:
	mov	eax, 0
.L42:
	mov	edi, eax
	call	__VERIFIER_assert
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	mov	BYTE PTR x$r_buff1_thd0[rip], al
	movzx	eax, BYTE PTR x$r_buff0_thd1[rip]
	mov	BYTE PTR x$r_buff1_thd1[rip], al
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	mov	BYTE PTR x$r_buff1_thd2[rip], al
	movzx	eax, BYTE PTR x$r_buff0_thd3[rip]
	mov	BYTE PTR x$r_buff1_thd3[rip], al
	movzx	eax, BYTE PTR x$r_buff0_thd4[rip]
	mov	BYTE PTR x$r_buff1_thd4[rip], al
	mov	BYTE PTR x$r_buff0_thd2[rip], 1
	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 x$flush_delayed[rip], al
	mov	eax, DWORD PTR x[rip]
	mov	DWORD PTR x$mem_tmp[rip], eax
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L43
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	test	al, al
	jne	.L44
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	test	al, al
	je	.L43
.L44:
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	test	al, al
	jne	.L45
	movzx	eax, BYTE PTR x$r_buff1_thd2[rip]
	test	al, al
	je	.L43
.L45:
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L46
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	test	al, al
	je	.L46
	mov	eax, DWORD PTR x$w_buff0[rip]
	jmp	.L48
.L46:
	mov	eax, DWORD PTR x$w_buff1[rip]
	jmp	.L48
.L43:
	mov	eax, DWORD PTR x[rip]
.L48:
	mov	DWORD PTR x[rip], eax
	mov	eax, DWORD PTR x$w_buff0[rip]
	mov	DWORD PTR x$w_buff0[rip], eax
	mov	eax, DWORD PTR x$w_buff1[rip]
	mov	DWORD PTR x$w_buff1[rip], eax
	movzx	eax, BYTE PTR weak$$choice2[rip]
	test	al, al
	je	.L49
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L50
.L49:
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L51
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L52
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L51
.L52:
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L53
	movzx	eax, BYTE PTR x$r_buff1_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L53
.L51:
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L50
.L53:
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L55
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	test	al, al
	jne	.L56
.L55:
	mov	eax, 1
	jmp	.L57
.L56:
	mov	eax, 0
.L57:
	and	eax, 1
	test	al, al
	je	.L58
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L58
	mov	eax, 1
	jmp	.L50
.L58:
	mov	eax, 0
.L50:
	mov	BYTE PTR x$w_buff0_used[rip], al
	movzx	eax, BYTE PTR weak$$choice2[rip]
	test	al, al
	je	.L60
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L61
.L60:
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L62
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L63
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L62
.L63:
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L64
	movzx	eax, BYTE PTR x$r_buff1_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L64
.L62:
	mov	eax, 1
	jmp	.L65
.L64:
	mov	eax, 0
.L65:
	and	eax, 1
	test	al, al
	je	.L66
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L66
	mov	eax, 1
	jmp	.L61
.L66:
	mov	eax, 0
.L61:
	mov	BYTE PTR x$w_buff1_used[rip], al
	movzx	eax, BYTE PTR weak$$choice2[rip]
	test	al, al
	je	.L68
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L69
.L68:
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L70
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L71
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L70
.L71:
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L72
	movzx	eax, BYTE PTR x$r_buff1_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L72
.L70:
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L69
.L72:
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L74
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	test	al, al
	jne	.L75
.L74:
	mov	eax, 1
	jmp	.L76
.L75:
	mov	eax, 0
.L76:
	and	eax, 1
	test	al, al
	je	.L77
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	movzx	eax, al
	test	eax, eax
	je	.L77
	mov	eax, 1
	jmp	.L69
.L77:
	mov	eax, 0
.L69:
	mov	BYTE PTR x$r_buff0_thd2[rip], al
	movzx	eax, BYTE PTR weak$$choice2[rip]
	test	al, al
	je	.L79
	movzx	eax, BYTE PTR x$r_buff1_thd2[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L80
.L79:
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L81
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L82
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L81
.L82:
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L83
	movzx	eax, BYTE PTR x$r_buff1_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L83
.L81:
	mov	eax, 1
	jmp	.L84
.L83:
	mov	eax, 0
.L84:
	and	eax, 1
	test	al, al
	je	.L85
	movzx	eax, BYTE PTR x$r_buff1_thd2[rip]
	movzx	eax, al
	test	eax, eax
	je	.L85
	mov	eax, 1
	jmp	.L80
.L85:
	mov	eax, 0
.L80:
	mov	BYTE PTR x$r_buff1_thd2[rip], al
	mov	eax, DWORD PTR x[rip]
	mov	DWORD PTR __unbuffered_p1_EAX[rip], eax
	movzx	eax, BYTE PTR x$flush_delayed[rip]
	test	al, al
	je	.L87
	mov	eax, DWORD PTR x$mem_tmp[rip]
	jmp	.L88
.L87:
	mov	eax, DWORD PTR x[rip]
.L88:
	mov	DWORD PTR x[rip], eax
	mov	BYTE PTR x$flush_delayed[rip], 0
	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 y$flush_delayed[rip], al
	mov	eax, DWORD PTR y[rip]
	mov	DWORD PTR y$mem_tmp[rip], eax
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L89
	movzx	eax, BYTE PTR y$r_buff0_thd2[rip]
	test	al, al
	jne	.L90
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	test	al, al
	je	.L89
.L90:
	movzx	eax, BYTE PTR y$r_buff0_thd2[rip]
	test	al, al
	jne	.L91
	movzx	eax, BYTE PTR y$r_buff1_thd2[rip]
	test	al, al
	je	.L89
.L91:
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L92
	movzx	eax, BYTE PTR y$r_buff0_thd2[rip]
	test	al, al
	je	.L92
	mov	eax, DWORD PTR y$w_buff0[rip]
	jmp	.L94
.L92:
	mov	eax, DWORD PTR y$w_buff1[rip]
	jmp	.L94
.L89:
	mov	eax, DWORD PTR y[rip]
.L94:
	mov	DWORD PTR y[rip], eax
	mov	eax, DWORD PTR y$w_buff0[rip]
	mov	DWORD PTR y$w_buff0[rip], eax
	mov	eax, DWORD PTR y$w_buff1[rip]
	mov	DWORD PTR y$w_buff1[rip], eax
	movzx	eax, BYTE PTR weak$$choice2[rip]
	test	al, al
	je	.L95
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L96
.L95:
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L97
	movzx	eax, BYTE PTR y$r_buff0_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L98
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L97
.L98:
	movzx	eax, BYTE PTR y$r_buff0_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L99
	movzx	eax, BYTE PTR y$r_buff1_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L99
.L97:
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L96
.L99:
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L101
	movzx	eax, BYTE PTR y$r_buff0_thd2[rip]
	test	al, al
	jne	.L102
.L101:
	mov	eax, 1
	jmp	.L103
.L102:
	mov	eax, 0
.L103:
	and	eax, 1
	test	al, al
	je	.L104
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L104
	mov	eax, 1
	jmp	.L96
.L104:
	mov	eax, 0
.L96:
	mov	BYTE PTR y$w_buff0_used[rip], al
	movzx	eax, BYTE PTR weak$$choice2[rip]
	test	al, al
	je	.L106
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L107
.L106:
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L108
	movzx	eax, BYTE PTR y$r_buff0_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L109
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L108
.L109:
	movzx	eax, BYTE PTR y$r_buff0_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L110
	movzx	eax, BYTE PTR y$r_buff1_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L110
.L108:
	mov	eax, 1
	jmp	.L111
.L110:
	mov	eax, 0
.L111:
	and	eax, 1
	test	al, al
	je	.L112
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L112
	mov	eax, 1
	jmp	.L107
.L112:
	mov	eax, 0
.L107:
	mov	BYTE PTR y$w_buff1_used[rip], al
	movzx	eax, BYTE PTR weak$$choice2[rip]
	test	al, al
	je	.L114
	movzx	eax, BYTE PTR y$r_buff0_thd2[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L115
.L114:
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L116
	movzx	eax, BYTE PTR y$r_buff0_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L117
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L116
.L117:
	movzx	eax, BYTE PTR y$r_buff0_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L118
	movzx	eax, BYTE PTR y$r_buff1_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L118
.L116:
	movzx	eax, BYTE PTR y$r_buff0_thd2[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L115
.L118:
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L120
	movzx	eax, BYTE PTR y$r_buff0_thd2[rip]
	test	al, al
	jne	.L121
.L120:
	mov	eax, 1
	jmp	.L122
.L121:
	mov	eax, 0
.L122:
	and	eax, 1
	test	al, al
	je	.L123
	movzx	eax, BYTE PTR y$r_buff0_thd2[rip]
	movzx	eax, al
	test	eax, eax
	je	.L123
	mov	eax, 1
	jmp	.L115
.L123:
	mov	eax, 0
.L115:
	mov	BYTE PTR y$r_buff0_thd2[rip], al
	movzx	eax, BYTE PTR weak$$choice2[rip]
	test	al, al
	je	.L125
	movzx	eax, BYTE PTR y$r_buff1_thd2[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L126
.L125:
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L127
	movzx	eax, BYTE PTR y$r_buff0_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L128
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L127
.L128:
	movzx	eax, BYTE PTR y$r_buff0_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L129
	movzx	eax, BYTE PTR y$r_buff1_thd2[rip]
	xor	eax, 1
	test	al, al
	je	.L129
.L127:
	mov	eax, 1
	jmp	.L130
.L129:
	mov	eax, 0
.L130:
	and	eax, 1
	test	al, al
	je	.L131
	movzx	eax, BYTE PTR y$r_buff1_thd2[rip]
	movzx	eax, al
	test	eax, eax
	je	.L131
	mov	eax, 1
	jmp	.L126
.L131:
	mov	eax, 0
.L126:
	mov	BYTE PTR y$r_buff1_thd2[rip], al
	mov	eax, DWORD PTR y[rip]
	mov	DWORD PTR __unbuffered_p1_EBX[rip], eax
	movzx	eax, BYTE PTR y$flush_delayed[rip]
	test	al, al
	je	.L133
	mov	eax, DWORD PTR y$mem_tmp[rip]
	jmp	.L134
.L133:
	mov	eax, DWORD PTR y[rip]
.L134:
	mov	DWORD PTR y[rip], eax
	mov	BYTE PTR y$flush_delayed[rip], 0
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L135
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	test	al, al
	jne	.L136
.L135:
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	test	al, al
	je	.L137
	movzx	eax, BYTE PTR x$r_buff1_thd2[rip]
	test	al, al
	je	.L137
	mov	eax, DWORD PTR x$w_buff1[rip]
	jmp	.L139
.L137:
	mov	eax, DWORD PTR x[rip]
	jmp	.L139
.L136:
	mov	eax, DWORD PTR x$w_buff0[rip]
.L139:
	mov	DWORD PTR x[rip], eax
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L140
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	test	al, al
	jne	.L141
.L140:
	mov	eax, 1
	jmp	.L142
.L141:
	mov	eax, 0
.L142:
	and	eax, 1
	test	al, al
	je	.L143
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L143
	mov	eax, 1
	jmp	.L144
.L143:
	mov	eax, 0
.L144:
	mov	BYTE PTR x$w_buff0_used[rip], al
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L145
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	test	al, al
	jne	.L146
.L145:
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	test	al, al
	je	.L147
	movzx	eax, BYTE PTR x$r_buff1_thd2[rip]
	test	al, al
	jne	.L146
.L147:
	mov	eax, 1
	jmp	.L148
.L146:
	mov	eax, 0
.L148:
	and	eax, 1
	test	al, al
	je	.L149
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L149
	mov	eax, 1
	jmp	.L150
.L149:
	mov	eax, 0
.L150:
	mov	BYTE PTR x$w_buff1_used[rip], al
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L151
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	test	al, al
	jne	.L152
.L151:
	mov	eax, 1
	jmp	.L153
.L152:
	mov	eax, 0
.L153:
	and	eax, 1
	test	al, al
	je	.L154
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	movzx	eax, al
	test	eax, eax
	je	.L154
	mov	eax, 1
	jmp	.L155
.L154:
	mov	eax, 0
.L155:
	mov	BYTE PTR x$r_buff0_thd2[rip], al
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L156
	movzx	eax, BYTE PTR x$r_buff0_thd2[rip]
	test	al, al
	jne	.L157
.L156:
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	test	al, al
	je	.L158
	movzx	eax, BYTE PTR x$r_buff1_thd2[rip]
	test	al, al
	jne	.L157
.L158:
	mov	eax, 1
	jmp	.L159
.L157:
	mov	eax, 0
.L159:
	and	eax, 1
	test	al, al
	je	.L160
	movzx	eax, BYTE PTR x$r_buff1_thd2[rip]
	movzx	eax, al
	test	eax, eax
	je	.L160
	mov	eax, 1
	jmp	.L161
.L160:
	mov	eax, 0
.L161:
	mov	BYTE PTR x$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	eax, DWORD PTR y$w_buff0[rip]
	mov	DWORD PTR y$w_buff1[rip], eax
	mov	DWORD PTR y$w_buff0[rip], 1
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	mov	BYTE PTR y$w_buff1_used[rip], al
	mov	BYTE PTR y$w_buff0_used[rip], 1
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L164
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	je	.L165
.L164:
	mov	eax, 1
	jmp	.L166
.L165:
	mov	eax, 0
.L166:
	mov	edi, eax
	call	__VERIFIER_assert
	movzx	eax, BYTE PTR y$r_buff0_thd0[rip]
	mov	BYTE PTR y$r_buff1_thd0[rip], al
	movzx	eax, BYTE PTR y$r_buff0_thd1[rip]
	mov	BYTE PTR y$r_buff1_thd1[rip], al
	movzx	eax, BYTE PTR y$r_buff0_thd2[rip]
	mov	BYTE PTR y$r_buff1_thd2[rip], al
	movzx	eax, BYTE PTR y$r_buff0_thd3[rip]
	mov	BYTE PTR y$r_buff1_thd3[rip], al
	movzx	eax, BYTE PTR y$r_buff0_thd4[rip]
	mov	BYTE PTR y$r_buff1_thd4[rip], al
	mov	BYTE PTR y$r_buff0_thd3[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
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L167
	movzx	eax, BYTE PTR x$r_buff0_thd3[rip]
	test	al, al
	jne	.L168
.L167:
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	test	al, al
	je	.L169
	movzx	eax, BYTE PTR x$r_buff1_thd3[rip]
	test	al, al
	je	.L169
	mov	eax, DWORD PTR x$w_buff1[rip]
	jmp	.L171
.L169:
	mov	eax, DWORD PTR x[rip]
	jmp	.L171
.L168:
	mov	eax, DWORD PTR x$w_buff0[rip]
.L171:
	mov	DWORD PTR x[rip], eax
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L172
	movzx	eax, BYTE PTR x$r_buff0_thd3[rip]
	test	al, al
	jne	.L173
.L172:
	mov	eax, 1
	jmp	.L174
.L173:
	mov	eax, 0
.L174:
	and	eax, 1
	test	al, al
	je	.L175
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L175
	mov	eax, 1
	jmp	.L176
.L175:
	mov	eax, 0
.L176:
	mov	BYTE PTR x$w_buff0_used[rip], al
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L177
	movzx	eax, BYTE PTR x$r_buff0_thd3[rip]
	test	al, al
	jne	.L178
.L177:
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	test	al, al
	je	.L179
	movzx	eax, BYTE PTR x$r_buff1_thd3[rip]
	test	al, al
	jne	.L178
.L179:
	mov	eax, 1
	jmp	.L180
.L178:
	mov	eax, 0
.L180:
	and	eax, 1
	test	al, al
	je	.L181
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L181
	mov	eax, 1
	jmp	.L182
.L181:
	mov	eax, 0
.L182:
	mov	BYTE PTR x$w_buff1_used[rip], al
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L183
	movzx	eax, BYTE PTR x$r_buff0_thd3[rip]
	test	al, al
	jne	.L184
.L183:
	mov	eax, 1
	jmp	.L185
.L184:
	mov	eax, 0
.L185:
	and	eax, 1
	test	al, al
	je	.L186
	movzx	eax, BYTE PTR x$r_buff0_thd3[rip]
	movzx	eax, al
	test	eax, eax
	je	.L186
	mov	eax, 1
	jmp	.L187
.L186:
	mov	eax, 0
.L187:
	mov	BYTE PTR x$r_buff0_thd3[rip], al
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L188
	movzx	eax, BYTE PTR x$r_buff0_thd3[rip]
	test	al, al
	jne	.L189
.L188:
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	test	al, al
	je	.L190
	movzx	eax, BYTE PTR x$r_buff1_thd3[rip]
	test	al, al
	jne	.L189
.L190:
	mov	eax, 1
	jmp	.L191
.L189:
	mov	eax, 0
.L191:
	and	eax, 1
	test	al, al
	je	.L192
	movzx	eax, BYTE PTR x$r_buff1_thd3[rip]
	movzx	eax, al
	test	eax, eax
	je	.L192
	mov	eax, 1
	jmp	.L193
.L192:
	mov	eax, 0
.L193:
	mov	BYTE PTR x$r_buff1_thd3[rip], al
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L194
	movzx	eax, BYTE PTR y$r_buff0_thd3[rip]
	test	al, al
	jne	.L195
.L194:
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	test	al, al
	je	.L196
	movzx	eax, BYTE PTR y$r_buff1_thd3[rip]
	test	al, al
	je	.L196
	mov	eax, DWORD PTR y$w_buff1[rip]
	jmp	.L198
.L196:
	mov	eax, DWORD PTR y[rip]
	jmp	.L198
.L195:
	mov	eax, DWORD PTR y$w_buff0[rip]
.L198:
	mov	DWORD PTR y[rip], eax
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L199
	movzx	eax, BYTE PTR y$r_buff0_thd3[rip]
	test	al, al
	jne	.L200
.L199:
	mov	eax, 1
	jmp	.L201
.L200:
	mov	eax, 0
.L201:
	and	eax, 1
	test	al, al
	je	.L202
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L202
	mov	eax, 1
	jmp	.L203
.L202:
	mov	eax, 0
.L203:
	mov	BYTE PTR y$w_buff0_used[rip], al
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L204
	movzx	eax, BYTE PTR y$r_buff0_thd3[rip]
	test	al, al
	jne	.L205
.L204:
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	test	al, al
	je	.L206
	movzx	eax, BYTE PTR y$r_buff1_thd3[rip]
	test	al, al
	jne	.L205
.L206:
	mov	eax, 1
	jmp	.L207
.L205:
	mov	eax, 0
.L207:
	and	eax, 1
	test	al, al
	je	.L208
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L208
	mov	eax, 1
	jmp	.L209
.L208:
	mov	eax, 0
.L209:
	mov	BYTE PTR y$w_buff1_used[rip], al
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L210
	movzx	eax, BYTE PTR y$r_buff0_thd3[rip]
	test	al, al
	jne	.L211
.L210:
	mov	eax, 1
	jmp	.L212
.L211:
	mov	eax, 0
.L212:
	and	eax, 1
	test	al, al
	je	.L213
	movzx	eax, BYTE PTR y$r_buff0_thd3[rip]
	movzx	eax, al
	test	eax, eax
	je	.L213
	mov	eax, 1
	jmp	.L214
.L213:
	mov	eax, 0
.L214:
	mov	BYTE PTR y$r_buff0_thd3[rip], al
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L215
	movzx	eax, BYTE PTR y$r_buff0_thd3[rip]
	test	al, al
	jne	.L216
.L215:
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	test	al, al
	je	.L217
	movzx	eax, BYTE PTR y$r_buff1_thd3[rip]
	test	al, al
	jne	.L216
.L217:
	mov	eax, 1
	jmp	.L218
.L216:
	mov	eax, 0
.L218:
	and	eax, 1
	test	al, al
	je	.L219
	movzx	eax, BYTE PTR y$r_buff1_thd3[rip]
	movzx	eax, al
	test	eax, eax
	je	.L219
	mov	eax, 1
	jmp	.L220
.L219:
	mov	eax, 0
.L220:
	mov	BYTE PTR y$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	P3
	.type	P3, @function
P3:
.LFB6:
	.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_p3_EAX[rip], eax
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	mov	eax, DWORD PTR a[rip]
	mov	DWORD PTR __unbuffered_p3_EBX[rip], eax
	mov	eax, 0
	call	__VERIFIER_atomic_end
	mov	eax, 0
	call	__VERIFIER_atomic_begin
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L223
	movzx	eax, BYTE PTR x$r_buff0_thd4[rip]
	test	al, al
	jne	.L224
.L223:
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	test	al, al
	je	.L225
	movzx	eax, BYTE PTR x$r_buff1_thd4[rip]
	test	al, al
	je	.L225
	mov	eax, DWORD PTR x$w_buff1[rip]
	jmp	.L227
.L225:
	mov	eax, DWORD PTR x[rip]
	jmp	.L227
.L224:
	mov	eax, DWORD PTR x$w_buff0[rip]
.L227:
	mov	DWORD PTR x[rip], eax
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L228
	movzx	eax, BYTE PTR x$r_buff0_thd4[rip]
	test	al, al
	jne	.L229
.L228:
	mov	eax, 1
	jmp	.L230
.L229:
	mov	eax, 0
.L230:
	and	eax, 1
	test	al, al
	je	.L231
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L231
	mov	eax, 1
	jmp	.L232
.L231:
	mov	eax, 0
.L232:
	mov	BYTE PTR x$w_buff0_used[rip], al
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L233
	movzx	eax, BYTE PTR x$r_buff0_thd4[rip]
	test	al, al
	jne	.L234
.L233:
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	test	al, al
	je	.L235
	movzx	eax, BYTE PTR x$r_buff1_thd4[rip]
	test	al, al
	jne	.L234
.L235:
	mov	eax, 1
	jmp	.L236
.L234:
	mov	eax, 0
.L236:
	and	eax, 1
	test	al, al
	je	.L237
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L237
	mov	eax, 1
	jmp	.L238
.L237:
	mov	eax, 0
.L238:
	mov	BYTE PTR x$w_buff1_used[rip], al
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L239
	movzx	eax, BYTE PTR x$r_buff0_thd4[rip]
	test	al, al
	jne	.L240
.L239:
	mov	eax, 1
	jmp	.L241
.L240:
	mov	eax, 0
.L241:
	and	eax, 1
	test	al, al
	je	.L242
	movzx	eax, BYTE PTR x$r_buff0_thd4[rip]
	movzx	eax, al
	test	eax, eax
	je	.L242
	mov	eax, 1
	jmp	.L243
.L242:
	mov	eax, 0
.L243:
	mov	BYTE PTR x$r_buff0_thd4[rip], al
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L244
	movzx	eax, BYTE PTR x$r_buff0_thd4[rip]
	test	al, al
	jne	.L245
.L244:
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	test	al, al
	je	.L246
	movzx	eax, BYTE PTR x$r_buff1_thd4[rip]
	test	al, al
	jne	.L245
.L246:
	mov	eax, 1
	jmp	.L247
.L245:
	mov	eax, 0
.L247:
	and	eax, 1
	test	al, al
	je	.L248
	movzx	eax, BYTE PTR x$r_buff1_thd4[rip]
	movzx	eax, al
	test	eax, eax
	je	.L248
	mov	eax, 1
	jmp	.L249
.L248:
	mov	eax, 0
.L249:
	mov	BYTE PTR x$r_buff1_thd4[rip], al
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L250
	movzx	eax, BYTE PTR y$r_buff0_thd4[rip]
	test	al, al
	jne	.L251
.L250:
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	test	al, al
	je	.L252
	movzx	eax, BYTE PTR y$r_buff1_thd4[rip]
	test	al, al
	je	.L252
	mov	eax, DWORD PTR y$w_buff1[rip]
	jmp	.L254
.L252:
	mov	eax, DWORD PTR y[rip]
	jmp	.L254
.L251:
	mov	eax, DWORD PTR y$w_buff0[rip]
.L254:
	mov	DWORD PTR y[rip], eax
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L255
	movzx	eax, BYTE PTR y$r_buff0_thd4[rip]
	test	al, al
	jne	.L256
.L255:
	mov	eax, 1
	jmp	.L257
.L256:
	mov	eax, 0
.L257:
	and	eax, 1
	test	al, al
	je	.L258
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L258
	mov	eax, 1
	jmp	.L259
.L258:
	mov	eax, 0
.L259:
	mov	BYTE PTR y$w_buff0_used[rip], al
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L260
	movzx	eax, BYTE PTR y$r_buff0_thd4[rip]
	test	al, al
	jne	.L261
.L260:
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	test	al, al
	je	.L262
	movzx	eax, BYTE PTR y$r_buff1_thd4[rip]
	test	al, al
	jne	.L261
.L262:
	mov	eax, 1
	jmp	.L263
.L261:
	mov	eax, 0
.L263:
	and	eax, 1
	test	al, al
	je	.L264
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L264
	mov	eax, 1
	jmp	.L265
.L264:
	mov	eax, 0
.L265:
	mov	BYTE PTR y$w_buff1_used[rip], al
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L266
	movzx	eax, BYTE PTR y$r_buff0_thd4[rip]
	test	al, al
	jne	.L267
.L266:
	mov	eax, 1
	jmp	.L268
.L267:
	mov	eax, 0
.L268:
	and	eax, 1
	test	al, al
	je	.L269
	movzx	eax, BYTE PTR y$r_buff0_thd4[rip]
	movzx	eax, al
	test	eax, eax
	je	.L269
	mov	eax, 1
	jmp	.L270
.L269:
	mov	eax, 0
.L270:
	mov	BYTE PTR y$r_buff0_thd4[rip], al
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L271
	movzx	eax, BYTE PTR y$r_buff0_thd4[rip]
	test	al, al
	jne	.L272
.L271:
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	test	al, al
	je	.L273
	movzx	eax, BYTE PTR y$r_buff1_thd4[rip]
	test	al, al
	jne	.L272
.L273:
	mov	eax, 1
	jmp	.L274
.L272:
	mov	eax, 0
.L274:
	and	eax, 1
	test	al, al
	je	.L275
	movzx	eax, BYTE PTR y$r_buff1_thd4[rip]
	movzx	eax, al
	test	eax, eax
	je	.L275
	mov	eax, 1
	jmp	.L276
.L275:
	mov	eax, 0
.L276:
	mov	BYTE PTR y$r_buff1_thd4[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
.LFE6:
	.size	P3, .-P3
	.globl	fence
	.type	fence, @function
fence:
.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	fence, .-fence
	.globl	isync
	.type	isync, @function
isync:
.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	isync, .-isync
	.globl	lwfence
	.type	lwfence, @function
lwfence:
.LFB9:
	.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
.LFE9:
	.size	lwfence, .-lwfence
	.globl	main
	.type	main, @function
main:
.LFB10:
	.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	ecx, 0
	lea	rdx, P3[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, 4
	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 x$w_buff0_used[rip]
	test	al, al
	je	.L282
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	test	al, al
	jne	.L283
.L282:
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	test	al, al
	je	.L284
	movzx	eax, BYTE PTR x$r_buff1_thd0[rip]
	test	al, al
	je	.L284
	mov	eax, DWORD PTR x$w_buff1[rip]
	jmp	.L286
.L284:
	mov	eax, DWORD PTR x[rip]
	jmp	.L286
.L283:
	mov	eax, DWORD PTR x$w_buff0[rip]
.L286:
	mov	DWORD PTR x[rip], eax
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L287
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	test	al, al
	jne	.L288
.L287:
	mov	eax, 1
	jmp	.L289
.L288:
	mov	eax, 0
.L289:
	and	eax, 1
	test	al, al
	je	.L290
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L290
	mov	eax, 1
	jmp	.L291
.L290:
	mov	eax, 0
.L291:
	mov	BYTE PTR x$w_buff0_used[rip], al
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L292
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	test	al, al
	jne	.L293
.L292:
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	test	al, al
	je	.L294
	movzx	eax, BYTE PTR x$r_buff1_thd0[rip]
	test	al, al
	jne	.L293
.L294:
	mov	eax, 1
	jmp	.L295
.L293:
	mov	eax, 0
.L295:
	and	eax, 1
	test	al, al
	je	.L296
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L296
	mov	eax, 1
	jmp	.L297
.L296:
	mov	eax, 0
.L297:
	mov	BYTE PTR x$w_buff1_used[rip], al
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L298
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	test	al, al
	jne	.L299
.L298:
	mov	eax, 1
	jmp	.L300
.L299:
	mov	eax, 0
.L300:
	and	eax, 1
	test	al, al
	je	.L301
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	movzx	eax, al
	test	eax, eax
	je	.L301
	mov	eax, 1
	jmp	.L302
.L301:
	mov	eax, 0
.L302:
	mov	BYTE PTR x$r_buff0_thd0[rip], al
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L303
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	test	al, al
	jne	.L304
.L303:
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	test	al, al
	je	.L305
	movzx	eax, BYTE PTR x$r_buff1_thd0[rip]
	test	al, al
	jne	.L304
.L305:
	mov	eax, 1
	jmp	.L306
.L304:
	mov	eax, 0
.L306:
	and	eax, 1
	test	al, al
	je	.L307
	movzx	eax, BYTE PTR x$r_buff1_thd0[rip]
	movzx	eax, al
	test	eax, eax
	je	.L307
	mov	eax, 1
	jmp	.L308
.L307:
	mov	eax, 0
.L308:
	mov	BYTE PTR x$r_buff1_thd0[rip], al
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L309
	movzx	eax, BYTE PTR y$r_buff0_thd0[rip]
	test	al, al
	jne	.L310
.L309:
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	test	al, al
	je	.L311
	movzx	eax, BYTE PTR y$r_buff1_thd0[rip]
	test	al, al
	je	.L311
	mov	eax, DWORD PTR y$w_buff1[rip]
	jmp	.L313
.L311:
	mov	eax, DWORD PTR y[rip]
	jmp	.L313
.L310:
	mov	eax, DWORD PTR y$w_buff0[rip]
.L313:
	mov	DWORD PTR y[rip], eax
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L314
	movzx	eax, BYTE PTR y$r_buff0_thd0[rip]
	test	al, al
	jne	.L315
.L314:
	mov	eax, 1
	jmp	.L316
.L315:
	mov	eax, 0
.L316:
	and	eax, 1
	test	al, al
	je	.L317
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L317
	mov	eax, 1
	jmp	.L318
.L317:
	mov	eax, 0
.L318:
	mov	BYTE PTR y$w_buff0_used[rip], al
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L319
	movzx	eax, BYTE PTR y$r_buff0_thd0[rip]
	test	al, al
	jne	.L320
.L319:
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	test	al, al
	je	.L321
	movzx	eax, BYTE PTR y$r_buff1_thd0[rip]
	test	al, al
	jne	.L320
.L321:
	mov	eax, 1
	jmp	.L322
.L320:
	mov	eax, 0
.L322:
	and	eax, 1
	test	al, al
	je	.L323
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L323
	mov	eax, 1
	jmp	.L324
.L323:
	mov	eax, 0
.L324:
	mov	BYTE PTR y$w_buff1_used[rip], al
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L325
	movzx	eax, BYTE PTR y$r_buff0_thd0[rip]
	test	al, al
	jne	.L326
.L325:
	mov	eax, 1
	jmp	.L327
.L326:
	mov	eax, 0
.L327:
	and	eax, 1
	test	al, al
	je	.L328
	movzx	eax, BYTE PTR y$r_buff0_thd0[rip]
	movzx	eax, al
	test	eax, eax
	je	.L328
	mov	eax, 1
	jmp	.L329
.L328:
	mov	eax, 0
.L329:
	mov	BYTE PTR y$r_buff0_thd0[rip], al
	movzx	eax, BYTE PTR y$w_buff0_used[rip]
	test	al, al
	je	.L330
	movzx	eax, BYTE PTR y$r_buff0_thd0[rip]
	test	al, al
	jne	.L331
.L330:
	movzx	eax, BYTE PTR y$w_buff1_used[rip]
	test	al, al
	je	.L332
	movzx	eax, BYTE PTR y$r_buff1_thd0[rip]
	test	al, al
	jne	.L331
.L332:
	mov	eax, 1
	jmp	.L333
.L331:
	mov	eax, 0
.L333:
	and	eax, 1
	test	al, al
	je	.L334
	movzx	eax, BYTE PTR y$r_buff1_thd0[rip]
	movzx	eax, al
	test	eax, eax
	je	.L334
	mov	eax, 1
	jmp	.L335
.L334:
	mov	eax, 0
.L335:
	mov	BYTE PTR y$r_buff1_thd0[rip], al
	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 x$flush_delayed[rip], al
	mov	eax, DWORD PTR x[rip]
	mov	DWORD PTR x$mem_tmp[rip], eax
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L336
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	test	al, al
	jne	.L337
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	test	al, al
	je	.L336
.L337:
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	test	al, al
	jne	.L338
	movzx	eax, BYTE PTR x$r_buff1_thd0[rip]
	test	al, al
	je	.L336
.L338:
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L339
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	test	al, al
	je	.L339
	mov	eax, DWORD PTR x$w_buff0[rip]
	jmp	.L341
.L339:
	mov	eax, DWORD PTR x$w_buff1[rip]
	jmp	.L341
.L336:
	mov	eax, DWORD PTR x[rip]
.L341:
	mov	DWORD PTR x[rip], eax
	mov	eax, DWORD PTR x$w_buff0[rip]
	mov	DWORD PTR x$w_buff0[rip], eax
	mov	eax, DWORD PTR x$w_buff1[rip]
	mov	DWORD PTR x$w_buff1[rip], eax
	movzx	eax, BYTE PTR weak$$choice2[rip]
	test	al, al
	je	.L342
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L343
.L342:
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L344
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	xor	eax, 1
	test	al, al
	je	.L345
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L344
.L345:
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	xor	eax, 1
	test	al, al
	je	.L346
	movzx	eax, BYTE PTR x$r_buff1_thd0[rip]
	xor	eax, 1
	test	al, al
	je	.L346
.L344:
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L343
.L346:
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L348
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	test	al, al
	jne	.L349
.L348:
	mov	eax, 1
	jmp	.L350
.L349:
	mov	eax, 0
.L350:
	and	eax, 1
	test	al, al
	je	.L351
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L351
	mov	eax, 1
	jmp	.L343
.L351:
	mov	eax, 0
.L343:
	mov	BYTE PTR x$w_buff0_used[rip], al
	movzx	eax, BYTE PTR weak$$choice2[rip]
	test	al, al
	je	.L353
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L354
.L353:
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L355
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	xor	eax, 1
	test	al, al
	je	.L356
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L355
.L356:
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	xor	eax, 1
	test	al, al
	je	.L357
	movzx	eax, BYTE PTR x$r_buff1_thd0[rip]
	xor	eax, 1
	test	al, al
	je	.L357
.L355:
	mov	eax, 1
	jmp	.L358
.L357:
	mov	eax, 0
.L358:
	and	eax, 1
	test	al, al
	je	.L359
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	movzx	eax, al
	test	eax, eax
	je	.L359
	mov	eax, 1
	jmp	.L354
.L359:
	mov	eax, 0
.L354:
	mov	BYTE PTR x$w_buff1_used[rip], al
	movzx	eax, BYTE PTR weak$$choice2[rip]
	test	al, al
	je	.L361
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L362
.L361:
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L363
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	xor	eax, 1
	test	al, al
	je	.L364
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L363
.L364:
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	xor	eax, 1
	test	al, al
	je	.L365
	movzx	eax, BYTE PTR x$r_buff1_thd0[rip]
	xor	eax, 1
	test	al, al
	je	.L365
.L363:
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L362
.L365:
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	test	al, al
	je	.L367
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	test	al, al
	jne	.L368
.L367:
	mov	eax, 1
	jmp	.L369
.L368:
	mov	eax, 0
.L369:
	and	eax, 1
	test	al, al
	je	.L370
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	movzx	eax, al
	test	eax, eax
	je	.L370
	mov	eax, 1
	jmp	.L362
.L370:
	mov	eax, 0
.L362:
	mov	BYTE PTR x$r_buff0_thd0[rip], al
	movzx	eax, BYTE PTR weak$$choice2[rip]
	test	al, al
	je	.L372
	movzx	eax, BYTE PTR x$r_buff1_thd0[rip]
	movzx	eax, al
	test	eax, eax
	setne	al
	jmp	.L373
.L372:
	movzx	eax, BYTE PTR x$w_buff0_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L374
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	xor	eax, 1
	test	al, al
	je	.L375
	movzx	eax, BYTE PTR x$w_buff1_used[rip]
	xor	eax, 1
	test	al, al
	jne	.L374
.L375:
	movzx	eax, BYTE PTR x$r_buff0_thd0[rip]
	xor	eax, 1
	test	al, al
	je	.L376
	movzx	eax, BYTE PTR x$r_buff1_thd0[rip]
	xor	eax, 1
	test	al, al
	je	.L376
.L374:
	mov	eax, 1
	jmp	.L377
.L376:
	mov	eax, 0
.L377:
	and	eax, 1
	test	al, al
	je	.L378
	movzx	eax, BYTE PTR x$r_buff1_thd0[rip]
	movzx	eax, al
	test	eax, eax
	je	.L378
	mov	eax, 1
	jmp	.L373
.L378:
	mov	eax, 0
.L373:
	mov	BYTE PTR x$r_buff1_thd0[rip], al
	mov	eax, DWORD PTR x[rip]
	cmp	eax, 2
	jne	.L380
	mov	eax, DWORD PTR __unbuffered_p1_EAX[rip]
	cmp	eax, 2
	jne	.L380
	mov	eax, DWORD PTR __unbuffered_p1_EBX[rip]
	test	eax, eax
	jne	.L380
	mov	eax, DWORD PTR __unbuffered_p2_EAX[rip]
	test	eax, eax
	jne	.L380
	mov	eax, DWORD PTR __unbuffered_p3_EAX[rip]
	cmp	eax, 1
	jne	.L380
	mov	eax, DWORD PTR __unbuffered_p3_EBX[rip]
	test	eax, eax
	je	.L381
.L380:
	mov	eax, 1
	jmp	.L382
.L381:
	mov	eax, 0
.L382:
	and	eax, 1
	mov	BYTE PTR main$tmp_guard1[rip], al
	movzx	eax, BYTE PTR x$flush_delayed[rip]
	test	al, al
	je	.L383
	mov	eax, DWORD PTR x$mem_tmp[rip]
	jmp	.L384
.L383:
	mov	eax, DWORD PTR x[rip]
.L384:
	mov	DWORD PTR x[rip], eax
	mov	BYTE PTR x$flush_delayed[rip], 0
	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
.LFE10:
	.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	"1257268.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_p1_EAX
	.align	2
	.type	__unbuffered_p1_EAX, %object
	.size	__unbuffered_p1_EAX, 4
__unbuffered_p1_EAX:
	.space	4
	.global	__unbuffered_p1_EBX
	.align	2
	.type	__unbuffered_p1_EBX, %object
	.size	__unbuffered_p1_EBX, 4
__unbuffered_p1_EBX:
	.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_p3_EAX
	.align	2
	.type	__unbuffered_p3_EAX, %object
	.size	__unbuffered_p3_EAX, 4
__unbuffered_p3_EAX:
	.space	4
	.global	__unbuffered_p3_EBX
	.align	2
	.type	__unbuffered_p3_EBX, %object
	.size	__unbuffered_p3_EBX, 4
__unbuffered_p3_EBX:
	.space	4
	.global	a
	.align	2
	.type	a, %object
	.size	a, 4
a:
	.space	4
	.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
	.comm	x$flush_delayed,1,1
	.comm	x$mem_tmp,4,4
	.comm	x$r_buff0_thd0,1,1
	.comm	x$r_buff0_thd1,1,1
	.comm	x$r_buff0_thd2,1,1
	.comm	x$r_buff0_thd3,1,1
	.comm	x$r_buff0_thd4,1,1
	.comm	x$r_buff1_thd0,1,1
	.comm	x$r_buff1_thd1,1,1
	.comm	x$r_buff1_thd2,1,1
	.comm	x$r_buff1_thd3,1,1
	.comm	x$r_buff1_thd4,1,1
	.comm	x$read_delayed,1,1
	.comm	x$read_delayed_var,4,4
	.comm	x$w_buff0,4,4
	.comm	x$w_buff0_used,1,1
	.comm	x$w_buff1,4,4
	.comm	x$w_buff1_used,1,1
	.global	y
	.align	2
	.type	y, %object
	.size	y, 4
y:
	.space	4
	.comm	y$flush_delayed,1,1
	.comm	y$mem_tmp,4,4
	.comm	y$r_buff0_thd0,1,1
	.comm	y$r_buff0_thd1,1,1
	.comm	y$r_buff0_thd2,1,1
	.comm	y$r_buff0_thd3,1,1
	.comm	y$r_buff0_thd4,1,1
	.comm	y$r_buff1_thd0,1,1
	.comm	y$r_buff1_thd1,1,1
	.comm	y$r_buff1_thd2,1,1
	.comm	y$r_buff1_thd3,1,1
	.comm	y$r_buff1_thd4,1,1
	.comm	y$read_delayed,1,1
	.comm	y$read_delayed_var,4,4
	.comm	y$w_buff0,4,4
	.comm	y$w_buff0_used,1,1
	.comm	y$w_buff1,4,4
	.comm	y$w_buff1_used,1,1
	.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, .L43
	mov	r2, #1
	str	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L43+4
	mov	r2, #1
	str	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L43+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L15
	ldr	r3, .L43+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L16
.L15:
	ldr	r3, .L43+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L17
	ldr	r3, .L43+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L17
	ldr	r3, .L43+24
	ldr	r3, [r3]
	b	.L19
.L17:
	ldr	r3, .L43+4
	ldr	r3, [r3]
	b	.L19
.L16:
	ldr	r3, .L43+28
	ldr	r3, [r3]
.L19:
	ldr	r2, .L43+4
	str	r3, [r2]
	ldr	r3, .L43+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L20
	ldr	r3, .L43+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L21
.L20:
	mov	r3, #1
	b	.L22
.L21:
	mov	r3, #0
.L22:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L23
	ldr	r3, .L43+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L23
	mov	r2, #1
	b	.L24
.L23:
	mov	r2, #0
.L24:
	ldr	r3, .L43+8
	strb	r2, [r3]
	ldr	r3, .L43+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L25
	ldr	r3, .L43+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L26
.L25:
	ldr	r3, .L43+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L27
	ldr	r3, .L43+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L26
.L27:
	mov	r3, #1
	b	.L28
.L26:
	mov	r3, #0
.L28:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L29
	ldr	r3, .L43+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L29
	mov	r2, #1
	b	.L30
.L29:
	mov	r2, #0
.L30:
	ldr	r3, .L43+16
	strb	r2, [r3]
	ldr	r3, .L43+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L31
	ldr	r3, .L43+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L32
.L31:
	mov	r3, #1
	b	.L33
.L32:
	mov	r3, #0
.L33:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L34
	ldr	r3, .L43+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L34
	mov	r2, #1
	b	.L35
.L34:
	mov	r2, #0
.L35:
	ldr	r3, .L43+12
	strb	r2, [r3]
	ldr	r3, .L43+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L36
	ldr	r3, .L43+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L37
.L36:
	ldr	r3, .L43+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L38
	ldr	r3, .L43+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L37
.L38:
	mov	r3, #1
	b	.L39
.L37:
	mov	r3, #0
.L39:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L40
	ldr	r3, .L43+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L40
	mov	r2, #1
	b	.L41
.L40:
	mov	r2, #0
.L41:
	ldr	r3, .L43+20
	strb	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L43+32
	ldr	r3, [r3]
	add	r3, r3, #1
	ldr	r2, .L43+32
	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}
.L44:
	.align	2
.L43:
	.word	a
	.word	x
	.word	x$w_buff0_used
	.word	x$r_buff0_thd1
	.word	x$w_buff1_used
	.word	x$r_buff1_thd1
	.word	x$w_buff1
	.word	x$w_buff0
	.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, .L169
	ldr	r3, [r3]
	ldr	r2, .L169+4
	str	r3, [r2]
	ldr	r3, .L169
	mov	r2, #2
	str	r2, [r3]
	ldr	r3, .L169+8
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L169+12
	strb	r2, [r3]
	ldr	r3, .L169+8
	mov	r2, #1
	strb	r2, [r3]
	ldr	r3, .L169+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L46
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L47
.L46:
	mov	r3, #1
	b	.L48
.L47:
	mov	r3, #0
.L48:
	mov	r0, r3
	bl	__VERIFIER_assert
	ldr	r3, .L169+16
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L169+20
	strb	r2, [r3]
	ldr	r3, .L169+24
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L169+28
	strb	r2, [r3]
	ldr	r3, .L169+32
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L169+36
	strb	r2, [r3]
	ldr	r3, .L169+40
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L169+44
	strb	r2, [r3]
	ldr	r3, .L169+48
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L169+52
	strb	r2, [r3]
	ldr	r3, .L169+32
	mov	r2, #1
	strb	r2, [r3]
	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, .L169+56
	strb	r2, [r3]
	bl	nondet_1
	mov	r3, r0
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r2, r3, #255
	ldr	r3, .L169+60
	strb	r2, [r3]
	ldr	r3, .L169+60
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L169+64
	strb	r2, [r3]
	ldr	r3, .L169+68
	ldr	r3, [r3]
	ldr	r2, .L169+72
	str	r3, [r2]
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L49
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L50
	ldr	r3, .L169+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L49
.L50:
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L51
	ldr	r3, .L169+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L49
.L51:
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L52
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L52
	ldr	r3, .L169
	ldr	r3, [r3]
	b	.L54
.L52:
	ldr	r3, .L169+4
	ldr	r3, [r3]
	b	.L54
.L49:
	ldr	r3, .L169+68
	ldr	r3, [r3]
.L54:
	ldr	r2, .L169+68
	str	r3, [r2]
	ldr	r3, .L169
	ldr	r3, [r3]
	ldr	r2, .L169
	str	r3, [r2]
	ldr	r3, .L169+4
	ldr	r3, [r3]
	ldr	r2, .L169+4
	str	r3, [r2]
	ldr	r3, .L169+60
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L55
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L56
.L55:
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L57
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L58
	ldr	r3, .L169+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L57
.L58:
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L59
	ldr	r3, .L169+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L59
.L57:
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L56
.L59:
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L61
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L62
.L61:
	mov	r3, #1
	b	.L63
.L62:
	mov	r3, #0
.L63:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L64
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L64
	mov	r3, #1
	b	.L56
.L64:
	mov	r3, #0
.L56:
	ldr	r2, .L169+8
	strb	r3, [r2]
	ldr	r3, .L169+60
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L66
	ldr	r3, .L169+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L67
.L66:
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L68
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L69
	ldr	r3, .L169+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L68
.L69:
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L70
	ldr	r3, .L169+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L70
.L68:
	mov	r3, #1
	b	.L71
.L70:
	mov	r3, #0
.L71:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L72
	ldr	r3, .L169+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L72
	mov	r3, #1
	b	.L67
.L72:
	mov	r3, #0
.L67:
	ldr	r2, .L169+12
	strb	r3, [r2]
	ldr	r3, .L169+60
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L74
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L75
.L74:
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L76
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L77
	ldr	r3, .L169+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L76
.L77:
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L78
	ldr	r3, .L169+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L78
.L76:
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L75
.L78:
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L80
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L81
.L80:
	mov	r3, #1
	b	.L82
.L81:
	mov	r3, #0
.L82:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L83
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L83
	mov	r3, #1
	b	.L75
.L83:
	mov	r3, #0
.L75:
	ldr	r2, .L169+32
	strb	r3, [r2]
	ldr	r3, .L169+60
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L85
	ldr	r3, .L169+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L86
.L85:
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L87
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L88
	ldr	r3, .L169+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L87
.L88:
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L89
	ldr	r3, .L169+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L89
.L87:
	mov	r3, #1
	b	.L90
.L89:
	mov	r3, #0
.L90:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L91
	ldr	r3, .L169+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L91
	mov	r3, #1
	b	.L86
.L91:
	mov	r3, #0
.L86:
	ldr	r2, .L169+36
	strb	r3, [r2]
	ldr	r3, .L169+68
	ldr	r3, [r3]
	ldr	r2, .L169+76
	str	r3, [r2]
	ldr	r3, .L169+64
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L93
	ldr	r3, .L169+72
	ldr	r3, [r3]
	b	.L94
.L93:
	ldr	r3, .L169+68
	ldr	r3, [r3]
.L94:
	ldr	r2, .L169+68
	str	r3, [r2]
	ldr	r3, .L169+64
	mov	r2, #0
	strb	r2, [r3]
	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, .L169+56
	strb	r2, [r3]
	bl	nondet_1
	mov	r3, r0
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r2, r3, #255
	ldr	r3, .L169+60
	strb	r2, [r3]
	ldr	r3, .L169+60
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L169+80
	strb	r2, [r3]
	ldr	r3, .L169+84
	ldr	r3, [r3]
	ldr	r2, .L169+88
	str	r3, [r2]
	ldr	r3, .L169+92
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L95
	ldr	r3, .L169+96
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L96
	ldr	r3, .L169+100
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L95
.L96:
	ldr	r3, .L169+96
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L97
	ldr	r3, .L169+104
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L95
.L97:
	ldr	r3, .L169+92
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L98
	ldr	r3, .L169+96
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L98
	ldr	r3, .L169+108
	ldr	r3, [r3]
	b	.L100
.L98:
	ldr	r3, .L169+112
	ldr	r3, [r3]
	b	.L100
.L95:
	ldr	r3, .L169+84
	ldr	r3, [r3]
.L100:
	ldr	r2, .L169+84
	str	r3, [r2]
	ldr	r3, .L169+108
	ldr	r3, [r3]
	ldr	r2, .L169+108
	str	r3, [r2]
	ldr	r3, .L169+112
	ldr	r3, [r3]
	ldr	r2, .L169+112
	str	r3, [r2]
	ldr	r3, .L169+60
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L101
	ldr	r3, .L169+92
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L102
.L101:
	ldr	r3, .L169+92
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L103
	ldr	r3, .L169+96
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L104
	ldr	r3, .L169+100
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L103
.L104:
	ldr	r3, .L169+96
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L105
	ldr	r3, .L169+104
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L105
.L103:
	ldr	r3, .L169+92
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L102
.L105:
	ldr	r3, .L169+92
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L107
	ldr	r3, .L169+96
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L108
.L107:
	mov	r3, #1
	b	.L109
.L108:
	mov	r3, #0
.L109:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L110
	ldr	r3, .L169+92
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L110
	mov	r3, #1
	b	.L102
.L110:
	mov	r3, #0
.L102:
	ldr	r2, .L169+92
	strb	r3, [r2]
	ldr	r3, .L169+60
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L112
	ldr	r3, .L169+100
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L113
.L112:
	ldr	r3, .L169+92
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L114
	ldr	r3, .L169+96
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L115
	ldr	r3, .L169+100
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L114
.L115:
	ldr	r3, .L169+96
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L116
	ldr	r3, .L169+104
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L116
.L114:
	mov	r3, #1
	b	.L117
.L116:
	mov	r3, #0
.L117:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L118
	ldr	r3, .L169+100
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L118
	mov	r3, #1
	b	.L113
.L118:
	mov	r3, #0
.L113:
	ldr	r2, .L169+100
	strb	r3, [r2]
	ldr	r3, .L169+60
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L120
	ldr	r3, .L169+96
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L121
.L120:
	ldr	r3, .L169+92
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L122
	ldr	r3, .L169+96
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L123
	ldr	r3, .L169+100
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L122
.L123:
	ldr	r3, .L169+96
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L124
	ldr	r3, .L169+104
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L124
.L122:
	ldr	r3, .L169+96
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L121
.L124:
	ldr	r3, .L169+92
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L126
	ldr	r3, .L169+96
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L127
.L126:
	mov	r3, #1
	b	.L128
.L127:
	mov	r3, #0
.L128:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L129
	ldr	r3, .L169+96
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L129
	mov	r3, #1
	b	.L121
.L129:
	mov	r3, #0
.L121:
	ldr	r2, .L169+96
	strb	r3, [r2]
	ldr	r3, .L169+60
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L131
	ldr	r3, .L169+104
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L132
.L131:
	ldr	r3, .L169+92
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L133
	ldr	r3, .L169+96
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L134
	ldr	r3, .L169+100
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L133
.L134:
	ldr	r3, .L169+96
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L135
	ldr	r3, .L169+104
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L135
.L133:
	mov	r3, #1
	b	.L136
.L135:
	mov	r3, #0
.L136:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L137
	ldr	r3, .L169+104
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L137
	mov	r3, #1
	b	.L132
.L137:
	mov	r3, #0
.L132:
	ldr	r2, .L169+104
	strb	r3, [r2]
	ldr	r3, .L169+84
	ldr	r3, [r3]
	ldr	r2, .L169+116
	str	r3, [r2]
	ldr	r3, .L169+80
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L139
	ldr	r3, .L169+88
	ldr	r3, [r3]
	b	.L140
.L139:
	ldr	r3, .L169+84
	ldr	r3, [r3]
.L140:
	ldr	r2, .L169+84
	str	r3, [r2]
	ldr	r3, .L169+80
	mov	r2, #0
	strb	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L141
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L142
.L141:
	ldr	r3, .L169+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L143
	ldr	r3, .L169+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L143
	ldr	r3, .L169+4
	ldr	r3, [r3]
	b	.L145
.L143:
	ldr	r3, .L169+68
	ldr	r3, [r3]
	b	.L145
.L142:
	ldr	r3, .L169
	ldr	r3, [r3]
.L145:
	ldr	r2, .L169+68
	str	r3, [r2]
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L146
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L147
.L146:
	mov	r3, #1
	b	.L148
.L147:
	mov	r3, #0
.L148:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L149
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L149
	mov	r2, #1
	b	.L150
.L149:
	mov	r2, #0
.L150:
	ldr	r3, .L169+8
	strb	r2, [r3]
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L151
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L152
.L151:
	ldr	r3, .L169+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L153
	ldr	r3, .L169+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L152
.L153:
	mov	r3, #1
	b	.L154
.L152:
	mov	r3, #0
.L154:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L155
	ldr	r3, .L169+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L155
	mov	r2, #1
	b	.L156
.L155:
	mov	r2, #0
.L156:
	ldr	r3, .L169+12
	strb	r2, [r3]
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L157
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L158
.L157:
	mov	r3, #1
	b	.L159
.L158:
	mov	r3, #0
.L159:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L160
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L160
	mov	r2, #1
	b	.L161
.L160:
	mov	r2, #0
.L161:
	ldr	r3, .L169+32
	strb	r2, [r3]
	ldr	r3, .L169+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L162
	ldr	r3, .L169+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L163
.L162:
	ldr	r3, .L169+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L164
	ldr	r3, .L169+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L163
.L164:
	mov	r3, #1
	b	.L165
.L163:
	mov	r3, #0
.L165:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L166
	ldr	r3, .L169+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L166
	mov	r2, #1
	b	.L167
.L166:
	mov	r2, #0
.L167:
	ldr	r3, .L169+36
	strb	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L169+120
	ldr	r3, [r3]
	add	r3, r3, #1
	ldr	r2, .L169+120
	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}
.L170:
	.align	2
.L169:
	.word	x$w_buff0
	.word	x$w_buff1
	.word	x$w_buff0_used
	.word	x$w_buff1_used
	.word	x$r_buff0_thd0
	.word	x$r_buff1_thd0
	.word	x$r_buff0_thd1
	.word	x$r_buff1_thd1
	.word	x$r_buff0_thd2
	.word	x$r_buff1_thd2
	.word	x$r_buff0_thd3
	.word	x$r_buff1_thd3
	.word	x$r_buff0_thd4
	.word	x$r_buff1_thd4
	.word	weak$$choice0
	.word	weak$$choice2
	.word	x$flush_delayed
	.word	x
	.word	x$mem_tmp
	.word	__unbuffered_p1_EAX
	.word	y$flush_delayed
	.word	y
	.word	y$mem_tmp
	.word	y$w_buff0_used
	.word	y$r_buff0_thd2
	.word	y$w_buff1_used
	.word	y$r_buff1_thd2
	.word	y$w_buff0
	.word	y$w_buff1
	.word	__unbuffered_p1_EBX
	.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, .L230
	ldr	r3, [r3]
	ldr	r2, .L230+4
	str	r3, [r2]
	ldr	r3, .L230
	mov	r2, #1
	str	r2, [r3]
	ldr	r3, .L230+8
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L230+12
	strb	r2, [r3]
	ldr	r3, .L230+8
	mov	r2, #1
	strb	r2, [r3]
	ldr	r3, .L230+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L172
	ldr	r3, .L230+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L173
.L172:
	mov	r3, #1
	b	.L174
.L173:
	mov	r3, #0
.L174:
	mov	r0, r3
	bl	__VERIFIER_assert
	ldr	r3, .L230+16
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L230+20
	strb	r2, [r3]
	ldr	r3, .L230+24
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L230+28
	strb	r2, [r3]
	ldr	r3, .L230+32
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L230+36
	strb	r2, [r3]
	ldr	r3, .L230+40
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L230+44
	strb	r2, [r3]
	ldr	r3, .L230+48
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L230+52
	strb	r2, [r3]
	ldr	r3, .L230+40
	mov	r2, #1
	strb	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L230+56
	ldr	r3, [r3]
	ldr	r2, .L230+60
	str	r3, [r2]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L230+64
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L175
	ldr	r3, .L230+68
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L176
.L175:
	ldr	r3, .L230+72
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L177
	ldr	r3, .L230+76
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L177
	ldr	r3, .L230+80
	ldr	r3, [r3]
	b	.L179
.L177:
	ldr	r3, .L230+84
	ldr	r3, [r3]
	b	.L179
.L176:
	ldr	r3, .L230+88
	ldr	r3, [r3]
.L179:
	ldr	r2, .L230+84
	str	r3, [r2]
	ldr	r3, .L230+64
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L180
	ldr	r3, .L230+68
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L181
.L180:
	mov	r3, #1
	b	.L182
.L181:
	mov	r3, #0
.L182:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L183
	ldr	r3, .L230+64
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L183
	mov	r2, #1
	b	.L184
.L183:
	mov	r2, #0
.L184:
	ldr	r3, .L230+64
	strb	r2, [r3]
	ldr	r3, .L230+64
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L185
	ldr	r3, .L230+68
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L186
.L185:
	ldr	r3, .L230+72
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L187
	ldr	r3, .L230+76
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L186
.L187:
	mov	r3, #1
	b	.L188
.L186:
	mov	r3, #0
.L188:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L189
	ldr	r3, .L230+72
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L189
	mov	r2, #1
	b	.L190
.L189:
	mov	r2, #0
.L190:
	ldr	r3, .L230+72
	strb	r2, [r3]
	ldr	r3, .L230+64
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L191
	ldr	r3, .L230+68
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L192
.L191:
	mov	r3, #1
	b	.L193
.L192:
	mov	r3, #0
.L193:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L194
	ldr	r3, .L230+68
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L194
	mov	r2, #1
	b	.L195
.L194:
	mov	r2, #0
.L195:
	ldr	r3, .L230+68
	strb	r2, [r3]
	ldr	r3, .L230+64
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L196
	ldr	r3, .L230+68
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L197
.L196:
	ldr	r3, .L230+72
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L198
	ldr	r3, .L230+76
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L197
.L198:
	mov	r3, #1
	b	.L199
.L197:
	mov	r3, #0
.L199:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L200
	ldr	r3, .L230+76
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L200
	mov	r2, #1
	b	.L201
.L200:
	mov	r2, #0
.L201:
	ldr	r3, .L230+76
	strb	r2, [r3]
	ldr	r3, .L230+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L202
	ldr	r3, .L230+40
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L203
.L202:
	ldr	r3, .L230+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L204
	ldr	r3, .L230+44
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L204
	ldr	r3, .L230+4
	ldr	r3, [r3]
	b	.L206
.L204:
	ldr	r3, .L230+92
	ldr	r3, [r3]
	b	.L206
.L203:
	ldr	r3, .L230
	ldr	r3, [r3]
.L206:
	ldr	r2, .L230+92
	str	r3, [r2]
	ldr	r3, .L230+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L207
	ldr	r3, .L230+40
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L208
.L207:
	mov	r3, #1
	b	.L209
.L208:
	mov	r3, #0
.L209:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L210
	ldr	r3, .L230+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L210
	mov	r2, #1
	b	.L211
.L210:
	mov	r2, #0
.L211:
	ldr	r3, .L230+8
	strb	r2, [r3]
	ldr	r3, .L230+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L212
	ldr	r3, .L230+40
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L213
.L212:
	ldr	r3, .L230+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L214
	ldr	r3, .L230+44
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L213
.L214:
	mov	r3, #1
	b	.L215
.L213:
	mov	r3, #0
.L215:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L216
	ldr	r3, .L230+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L216
	mov	r2, #1
	b	.L217
.L216:
	mov	r2, #0
.L217:
	ldr	r3, .L230+12
	strb	r2, [r3]
	ldr	r3, .L230+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L218
	ldr	r3, .L230+40
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L219
.L218:
	mov	r3, #1
	b	.L220
.L219:
	mov	r3, #0
.L220:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L221
	ldr	r3, .L230+40
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L221
	mov	r2, #1
	b	.L222
.L221:
	mov	r2, #0
.L222:
	ldr	r3, .L230+40
	strb	r2, [r3]
	ldr	r3, .L230+8
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L223
	ldr	r3, .L230+40
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L224
.L223:
	ldr	r3, .L230+12
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L225
	ldr	r3, .L230+44
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L224
.L225:
	mov	r3, #1
	b	.L226
.L224:
	mov	r3, #0
.L226:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L227
	ldr	r3, .L230+44
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L227
	mov	r2, #1
	b	.L228
.L227:
	mov	r2, #0
.L228:
	ldr	r3, .L230+44
	strb	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L230+96
	ldr	r3, [r3]
	add	r3, r3, #1
	ldr	r2, .L230+96
	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}
.L231:
	.align	2
.L230:
	.word	y$w_buff0
	.word	y$w_buff1
	.word	y$w_buff0_used
	.word	y$w_buff1_used
	.word	y$r_buff0_thd0
	.word	y$r_buff1_thd0
	.word	y$r_buff0_thd1
	.word	y$r_buff1_thd1
	.word	y$r_buff0_thd2
	.word	y$r_buff1_thd2
	.word	y$r_buff0_thd3
	.word	y$r_buff1_thd3
	.word	y$r_buff0_thd4
	.word	y$r_buff1_thd4
	.word	z
	.word	__unbuffered_p2_EAX
	.word	x$w_buff0_used
	.word	x$r_buff0_thd3
	.word	x$w_buff1_used
	.word	x$r_buff1_thd3
	.word	x$w_buff1
	.word	x
	.word	x$w_buff0
	.word	y
	.word	__unbuffered_cnt
	.size	P2, .-P2
	.align	2
	.global	P3
	.syntax unified
	.arm
	.fpu softvfp
	.type	P3, %function
P3:
	@ 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, .L288
	mov	r2, #1
	str	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L288
	ldr	r3, [r3]
	ldr	r2, .L288+4
	str	r3, [r2]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L288+8
	ldr	r3, [r3]
	ldr	r2, .L288+12
	str	r3, [r2]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L288+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L233
	ldr	r3, .L288+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L234
.L233:
	ldr	r3, .L288+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L235
	ldr	r3, .L288+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L235
	ldr	r3, .L288+32
	ldr	r3, [r3]
	b	.L237
.L235:
	ldr	r3, .L288+36
	ldr	r3, [r3]
	b	.L237
.L234:
	ldr	r3, .L288+40
	ldr	r3, [r3]
.L237:
	ldr	r2, .L288+36
	str	r3, [r2]
	ldr	r3, .L288+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L238
	ldr	r3, .L288+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L239
.L238:
	mov	r3, #1
	b	.L240
.L239:
	mov	r3, #0
.L240:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L241
	ldr	r3, .L288+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L241
	mov	r2, #1
	b	.L242
.L241:
	mov	r2, #0
.L242:
	ldr	r3, .L288+16
	strb	r2, [r3]
	ldr	r3, .L288+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L243
	ldr	r3, .L288+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L244
.L243:
	ldr	r3, .L288+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L245
	ldr	r3, .L288+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L244
.L245:
	mov	r3, #1
	b	.L246
.L244:
	mov	r3, #0
.L246:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L247
	ldr	r3, .L288+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L247
	mov	r2, #1
	b	.L248
.L247:
	mov	r2, #0
.L248:
	ldr	r3, .L288+24
	strb	r2, [r3]
	ldr	r3, .L288+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L249
	ldr	r3, .L288+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L250
.L249:
	mov	r3, #1
	b	.L251
.L250:
	mov	r3, #0
.L251:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L252
	ldr	r3, .L288+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L252
	mov	r2, #1
	b	.L253
.L252:
	mov	r2, #0
.L253:
	ldr	r3, .L288+20
	strb	r2, [r3]
	ldr	r3, .L288+16
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L254
	ldr	r3, .L288+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L255
.L254:
	ldr	r3, .L288+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L256
	ldr	r3, .L288+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L255
.L256:
	mov	r3, #1
	b	.L257
.L255:
	mov	r3, #0
.L257:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L258
	ldr	r3, .L288+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L258
	mov	r2, #1
	b	.L259
.L258:
	mov	r2, #0
.L259:
	ldr	r3, .L288+28
	strb	r2, [r3]
	ldr	r3, .L288+44
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L260
	ldr	r3, .L288+48
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L261
.L260:
	ldr	r3, .L288+52
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L262
	ldr	r3, .L288+56
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L262
	ldr	r3, .L288+60
	ldr	r3, [r3]
	b	.L264
.L262:
	ldr	r3, .L288+64
	ldr	r3, [r3]
	b	.L264
.L261:
	ldr	r3, .L288+68
	ldr	r3, [r3]
.L264:
	ldr	r2, .L288+64
	str	r3, [r2]
	ldr	r3, .L288+44
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L265
	ldr	r3, .L288+48
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L266
.L265:
	mov	r3, #1
	b	.L267
.L266:
	mov	r3, #0
.L267:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L268
	ldr	r3, .L288+44
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L268
	mov	r2, #1
	b	.L269
.L268:
	mov	r2, #0
.L269:
	ldr	r3, .L288+44
	strb	r2, [r3]
	ldr	r3, .L288+44
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L270
	ldr	r3, .L288+48
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L271
.L270:
	ldr	r3, .L288+52
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L272
	ldr	r3, .L288+56
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L271
.L272:
	mov	r3, #1
	b	.L273
.L271:
	mov	r3, #0
.L273:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L274
	ldr	r3, .L288+52
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L274
	mov	r2, #1
	b	.L275
.L274:
	mov	r2, #0
.L275:
	ldr	r3, .L288+52
	strb	r2, [r3]
	ldr	r3, .L288+44
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L276
	ldr	r3, .L288+48
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L277
.L276:
	mov	r3, #1
	b	.L278
.L277:
	mov	r3, #0
.L278:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L279
	ldr	r3, .L288+48
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L279
	mov	r2, #1
	b	.L280
.L279:
	mov	r2, #0
.L280:
	ldr	r3, .L288+48
	strb	r2, [r3]
	ldr	r3, .L288+44
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L281
	ldr	r3, .L288+48
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L282
.L281:
	ldr	r3, .L288+52
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L283
	ldr	r3, .L288+56
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L282
.L283:
	mov	r3, #1
	b	.L284
.L282:
	mov	r3, #0
.L284:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L285
	ldr	r3, .L288+56
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L285
	mov	r2, #1
	b	.L286
.L285:
	mov	r2, #0
.L286:
	ldr	r3, .L288+56
	strb	r2, [r3]
	bl	__VERIFIER_atomic_end
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L288+72
	ldr	r3, [r3]
	add	r3, r3, #1
	ldr	r2, .L288+72
	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}
.L289:
	.align	2
.L288:
	.word	z
	.word	__unbuffered_p3_EAX
	.word	a
	.word	__unbuffered_p3_EBX
	.word	x$w_buff0_used
	.word	x$r_buff0_thd4
	.word	x$w_buff1_used
	.word	x$r_buff1_thd4
	.word	x$w_buff1
	.word	x
	.word	x$w_buff0
	.word	y$w_buff0_used
	.word	y$r_buff0_thd4
	.word	y$w_buff1_used
	.word	y$r_buff1_thd4
	.word	y$w_buff1
	.word	y
	.word	y$w_buff0
	.word	__unbuffered_cnt
	.size	P3, .-P3
	.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, .L398
	mov	r1, #0
	mov	r0, #0
	bl	pthread_create
	mov	r3, #0
	ldr	r2, .L398+4
	mov	r1, #0
	mov	r0, #0
	bl	pthread_create
	mov	r3, #0
	ldr	r2, .L398+8
	mov	r1, #0
	mov	r0, #0
	bl	pthread_create
	mov	r3, #0
	ldr	r2, .L398+12
	mov	r1, #0
	mov	r0, #0
	bl	pthread_create
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L398+16
	ldr	r3, [r3]
	cmp	r3, #4
	moveq	r3, #1
	movne	r3, #0
	and	r2, r3, #255
	ldr	r3, .L398+20
	strb	r2, [r3]
	bl	__VERIFIER_atomic_end
	ldr	r3, .L398+20
	ldrb	r3, [r3]	@ zero_extendqisi2
	mov	r0, r3
	bl	__VERIFIER_assume
	bl	__VERIFIER_atomic_begin
	ldr	r3, .L398+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L294
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L295
.L294:
	ldr	r3, .L398+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L296
	ldr	r3, .L398+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L296
	ldr	r3, .L398+40
	ldr	r3, [r3]
	b	.L298
.L296:
	ldr	r3, .L398+44
	ldr	r3, [r3]
	b	.L298
.L295:
	ldr	r3, .L398+48
	ldr	r3, [r3]
.L298:
	ldr	r2, .L398+44
	str	r3, [r2]
	ldr	r3, .L398+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L299
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L300
.L299:
	mov	r3, #1
	b	.L301
.L300:
	mov	r3, #0
.L301:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L302
	ldr	r3, .L398+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L302
	mov	r2, #1
	b	.L303
.L302:
	mov	r2, #0
.L303:
	ldr	r3, .L398+24
	strb	r2, [r3]
	ldr	r3, .L398+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L304
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L305
.L304:
	ldr	r3, .L398+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L306
	ldr	r3, .L398+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L305
.L306:
	mov	r3, #1
	b	.L307
.L305:
	mov	r3, #0
.L307:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L308
	ldr	r3, .L398+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L308
	mov	r2, #1
	b	.L309
.L308:
	mov	r2, #0
.L309:
	ldr	r3, .L398+32
	strb	r2, [r3]
	ldr	r3, .L398+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L310
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L311
.L310:
	mov	r3, #1
	b	.L312
.L311:
	mov	r3, #0
.L312:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L313
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L313
	mov	r2, #1
	b	.L314
.L313:
	mov	r2, #0
.L314:
	ldr	r3, .L398+28
	strb	r2, [r3]
	ldr	r3, .L398+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L315
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L316
.L315:
	ldr	r3, .L398+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L317
	ldr	r3, .L398+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L316
.L317:
	mov	r3, #1
	b	.L318
.L316:
	mov	r3, #0
.L318:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L319
	ldr	r3, .L398+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L319
	mov	r2, #1
	b	.L320
.L319:
	mov	r2, #0
.L320:
	ldr	r3, .L398+36
	strb	r2, [r3]
	ldr	r3, .L398+52
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L321
	ldr	r3, .L398+56
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L322
.L321:
	ldr	r3, .L398+60
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L323
	ldr	r3, .L398+64
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L323
	ldr	r3, .L398+68
	ldr	r3, [r3]
	b	.L325
.L323:
	ldr	r3, .L398+72
	ldr	r3, [r3]
	b	.L325
.L322:
	ldr	r3, .L398+76
	ldr	r3, [r3]
.L325:
	ldr	r2, .L398+72
	str	r3, [r2]
	ldr	r3, .L398+52
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L326
	ldr	r3, .L398+56
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L327
.L326:
	mov	r3, #1
	b	.L328
.L327:
	mov	r3, #0
.L328:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L329
	ldr	r3, .L398+52
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L329
	mov	r2, #1
	b	.L330
.L329:
	mov	r2, #0
.L330:
	ldr	r3, .L398+52
	strb	r2, [r3]
	ldr	r3, .L398+52
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L331
	ldr	r3, .L398+56
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L332
.L331:
	ldr	r3, .L398+60
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L333
	ldr	r3, .L398+64
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L332
.L333:
	mov	r3, #1
	b	.L334
.L332:
	mov	r3, #0
.L334:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L335
	ldr	r3, .L398+60
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L335
	mov	r2, #1
	b	.L336
.L335:
	mov	r2, #0
.L336:
	ldr	r3, .L398+60
	strb	r2, [r3]
	ldr	r3, .L398+52
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L337
	ldr	r3, .L398+56
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L338
.L337:
	mov	r3, #1
	b	.L339
.L338:
	mov	r3, #0
.L339:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L340
	ldr	r3, .L398+56
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L340
	mov	r2, #1
	b	.L341
.L340:
	mov	r2, #0
.L341:
	ldr	r3, .L398+56
	strb	r2, [r3]
	ldr	r3, .L398+52
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L342
	ldr	r3, .L398+56
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L343
.L342:
	ldr	r3, .L398+60
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L344
	ldr	r3, .L398+64
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L343
.L344:
	mov	r3, #1
	b	.L345
.L343:
	mov	r3, #0
.L345:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L346
	ldr	r3, .L398+64
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L346
	mov	r2, #1
	b	.L347
.L346:
	mov	r2, #0
.L347:
	ldr	r3, .L398+64
	strb	r2, [r3]
	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, .L398+80
	strb	r2, [r3]
	bl	nondet_1
	mov	r3, r0
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r2, r3, #255
	ldr	r3, .L398+84
	strb	r2, [r3]
	ldr	r3, .L398+84
	ldrb	r2, [r3]	@ zero_extendqisi2
	ldr	r3, .L398+88
	strb	r2, [r3]
	ldr	r3, .L398+44
	ldr	r3, [r3]
	ldr	r2, .L398+92
	str	r3, [r2]
	ldr	r3, .L398+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L348
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L349
	ldr	r3, .L398+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L348
.L349:
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L350
	ldr	r3, .L398+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L348
.L350:
	ldr	r3, .L398+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L351
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L351
	ldr	r3, .L398+48
	ldr	r3, [r3]
	b	.L353
.L351:
	ldr	r3, .L398+40
	ldr	r3, [r3]
	b	.L353
.L348:
	ldr	r3, .L398+44
	ldr	r3, [r3]
.L353:
	ldr	r2, .L398+44
	str	r3, [r2]
	ldr	r3, .L398+48
	ldr	r3, [r3]
	ldr	r2, .L398+48
	str	r3, [r2]
	ldr	r3, .L398+40
	ldr	r3, [r3]
	ldr	r2, .L398+40
	str	r3, [r2]
	ldr	r3, .L398+84
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L354
	ldr	r3, .L398+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L355
.L354:
	ldr	r3, .L398+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L356
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L357
	ldr	r3, .L398+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L356
.L357:
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L358
	ldr	r3, .L398+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L358
.L356:
	ldr	r3, .L398+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L355
.L358:
	ldr	r3, .L398+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L360
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L361
.L360:
	mov	r3, #1
	b	.L362
.L361:
	mov	r3, #0
.L362:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L363
	ldr	r3, .L398+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L363
	mov	r3, #1
	b	.L355
.L363:
	mov	r3, #0
.L355:
	ldr	r2, .L398+24
	strb	r3, [r2]
	ldr	r3, .L398+84
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L365
	ldr	r3, .L398+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L366
.L365:
	ldr	r3, .L398+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L367
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L368
	ldr	r3, .L398+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L367
.L368:
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L369
	ldr	r3, .L398+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L369
.L367:
	mov	r3, #1
	b	.L370
.L369:
	mov	r3, #0
.L370:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L371
	ldr	r3, .L398+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L371
	mov	r3, #1
	b	.L366
.L371:
	mov	r3, #0
.L366:
	ldr	r2, .L398+32
	strb	r3, [r2]
	ldr	r3, .L398+84
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L373
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L374
.L373:
	ldr	r3, .L398+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L375
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L376
	ldr	r3, .L398+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L375
.L376:
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L377
	ldr	r3, .L398+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L377
.L375:
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L374
.L377:
	ldr	r3, .L398+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L379
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	bne	.L380
.L379:
	mov	r3, #1
	b	.L381
.L380:
	mov	r3, #0
.L381:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L382
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L382
	mov	r3, #1
	b	.L374
.L382:
	mov	r3, #0
.L374:
	ldr	r2, .L398+28
	strb	r3, [r2]
	ldr	r3, .L398+84
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L384
	ldr	r3, .L398+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	movne	r3, #1
	moveq	r3, #0
	and	r3, r3, #255
	b	.L385
.L384:
	ldr	r3, .L398+24
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L386
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L387
	ldr	r3, .L398+32
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L386
.L387:
	ldr	r3, .L398+28
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L388
	ldr	r3, .L398+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L388
.L386:
	mov	r3, #1
	b	.L389
.L388:
	mov	r3, #0
.L389:
	and	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	beq	.L390
	ldr	r3, .L398+36
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L390
	mov	r3, #1
	b	.L385
.L390:
	mov	r3, #0
.L385:
	ldr	r2, .L398+36
	strb	r3, [r2]
	ldr	r3, .L398+44
	ldr	r3, [r3]
	cmp	r3, #2
	bne	.L392
	ldr	r3, .L398+96
	ldr	r3, [r3]
	cmp	r3, #2
	bne	.L392
	ldr	r3, .L398+100
	ldr	r3, [r3]
	cmp	r3, #0
	bne	.L392
	ldr	r3, .L398+104
	ldr	r3, [r3]
	cmp	r3, #0
	bne	.L392
	ldr	r3, .L398+108
	ldr	r3, [r3]
	cmp	r3, #1
	bne	.L392
	ldr	r3, .L398+112
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L393
.L392:
	mov	r3, #1
	b	.L394
.L393:
	mov	r3, #0
.L394:
	and	r3, r3, #1
	and	r2, r3, #255
	ldr	r3, .L398+116
	strb	r2, [r3]
	ldr	r3, .L398+88
	ldrb	r3, [r3]	@ zero_extendqisi2
	cmp	r3, #0
	beq	.L395
	ldr	r3, .L398+92
	ldr	r3, [r3]
	b	.L396
.L395:
	ldr	r3, .L398+44
	ldr	r3, [r3]
.L396:
	ldr	r2, .L398+44
	str	r3, [r2]
	ldr	r3, .L398+88
	mov	r2, #0
	strb	r2, [r3]
	bl	__VERIFIER_atomic_end
	ldr	r3, .L398+116
	ldrb	r3, [r3]	@ zero_extendqisi2
	mov	r0, r3
	bl	__VERIFIER_assert
	mov	r3, #0
	mov	r0, r3
	pop	{fp, pc}
.L399:
	.align	2
.L398:
	.word	P0
	.word	P1
	.word	P2
	.word	P3
	.word	__unbuffered_cnt
	.word	main$tmp_guard0
	.word	x$w_buff0_used
	.word	x$r_buff0_thd0
	.word	x$w_buff1_used
	.word	x$r_buff1_thd0
	.word	x$w_buff1
	.word	x
	.word	x$w_buff0
	.word	y$w_buff0_used
	.word	y$r_buff0_thd0
	.word	y$w_buff1_used
	.word	y$r_buff1_thd0
	.word	y$w_buff1
	.word	y
	.word	y$w_buff0
	.word	weak$$choice0
	.word	weak$$choice2
	.word	x$flush_delayed
	.word	x$mem_tmp
	.word	__unbuffered_p1_EAX
	.word	__unbuffered_p1_EBX
	.word	__unbuffered_p2_EAX
	.word	__unbuffered_p3_EAX
	.word	__unbuffered_p3_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
