	.file	"145429.c"
	.intel_syntax noprefix
	.text
	.globl	reach_error
	.type	reach_error, @function
reach_error:
.LFB0:
	.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
.LFE0:
	.size	reach_error, .-reach_error
	.globl	assume_abort_if_not
	.type	assume_abort_if_not, @function
assume_abort_if_not:
.LFB1:
	.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	.L4
	call	abort@PLT
.L4:
	nop
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE1:
	.size	assume_abort_if_not, .-assume_abort_if_not
	.globl	__VERIFIER_assert
	.type	__VERIFIER_assert, @function
__VERIFIER_assert:
.LFB2:
	.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	.L9
	nop
.L7:
	mov	eax, 0
	call	reach_error
	call	abort@PLT
.L9:
	nop
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE2:
	.size	__VERIFIER_assert, .-__VERIFIER_assert
	.globl	SIZE
	.data
	.align 4
	.type	SIZE, @object
	.size	SIZE, 4
SIZE:
	.long	20000001
	.text
	.globl	main
	.type	main, @function
main:
.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, 32
	mov	DWORD PTR -4[rbp], 0
	mov	DWORD PTR -32[rbp], 0
	mov	DWORD PTR -28[rbp], 0
	mov	DWORD PTR -24[rbp], 0
	mov	DWORD PTR -20[rbp], 0
	mov	DWORD PTR -16[rbp], 0
	mov	DWORD PTR -12[rbp], 0
	mov	DWORD PTR -8[rbp], 0
	mov	eax, 0
	call	__VERIFIER_nondet_int@PLT
	mov	DWORD PTR -4[rbp], eax
	mov	eax, DWORD PTR SIZE[rip]
	cmp	DWORD PTR -4[rbp], eax
	jbe	.L13
	mov	eax, 0
	jmp	.L12
.L20:
	mov	ecx, DWORD PTR -20[rbp]
	mov	edx, ecx
	mov	eax, 2863311531
	imul	rax, rdx
	shr	rax, 32
	mov	edx, eax
	shr	edx, 2
	mov	eax, edx
	add	eax, eax
	add	eax, edx
	add	eax, eax
	sub	ecx, eax
	mov	edx, ecx
	test	edx, edx
	jne	.L14
	add	DWORD PTR -16[rbp], 1
	jmp	.L15
.L14:
	mov	ecx, DWORD PTR -20[rbp]
	mov	edx, ecx
	mov	eax, 3435973837
	imul	rax, rdx
	shr	rax, 32
	shr	eax, 2
	mov	edx, eax
	sal	edx, 2
	add	edx, eax
	mov	eax, ecx
	sub	eax, edx
	test	eax, eax
	jne	.L16
	add	DWORD PTR -12[rbp], 1
	jmp	.L15
.L16:
	mov	eax, DWORD PTR -20[rbp]
	and	eax, 3
	test	eax, eax
	jne	.L17
	add	DWORD PTR -8[rbp], 1
	jmp	.L15
.L17:
	mov	ecx, DWORD PTR -20[rbp]
	mov	edx, ecx
	mov	eax, 2863311531
	imul	rax, rdx
	shr	rax, 32
	shr	eax
	mov	edx, eax
	add	edx, edx
	add	edx, eax
	mov	eax, ecx
	sub	eax, edx
	test	eax, eax
	jne	.L18
	add	DWORD PTR -32[rbp], 1
	jmp	.L15
.L18:
	mov	eax, DWORD PTR -20[rbp]
	and	eax, 1
	test	eax, eax
	jne	.L19
	add	DWORD PTR -24[rbp], 1
	jmp	.L15
.L19:
	add	DWORD PTR -28[rbp], 1
.L15:
	add	DWORD PTR -20[rbp], 1
.L13:
	mov	eax, DWORD PTR -20[rbp]
	cmp	eax, DWORD PTR -4[rbp]
	jb	.L20
	mov	edx, DWORD PTR -32[rbp]
	mov	eax, DWORD PTR -24[rbp]
	add	edx, eax
	mov	eax, DWORD PTR -28[rbp]
	add	edx, eax
	mov	eax, DWORD PTR -8[rbp]
	add	edx, eax
	mov	eax, DWORD PTR -12[rbp]
	add	edx, eax
	mov	eax, DWORD PTR -16[rbp]
	add	eax, edx
	cmp	DWORD PTR -20[rbp], eax
	sete	al
	movzx	eax, al
	mov	edi, eax
	call	__VERIFIER_assert
	mov	eax, 0
.L12:
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE3:
	.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	"145429.c"
	.text
	.align	2
	.global	reach_error
	.syntax unified
	.arm
	.fpu softvfp
	.type	reach_error, %function
reach_error:
	@ 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	reach_error, .-reach_error
	.align	2
	.global	assume_abort_if_not
	.syntax unified
	.arm
	.fpu softvfp
	.type	assume_abort_if_not, %function
assume_abort_if_not:
	@ 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	.L4
	bl	abort
.L4:
	nop
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
	.size	assume_abort_if_not, .-assume_abort_if_not
	.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	.L9
	nop
.L7:
	bl	reach_error
	bl	abort
.L9:
	nop
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
	.size	__VERIFIER_assert, .-__VERIFIER_assert
	.global	SIZE
	.data
	.align	2
	.type	SIZE, %object
	.size	SIZE, 4
SIZE:
	.word	20000001
	.text
	.align	2
	.global	main
	.syntax unified
	.arm
	.fpu softvfp
	.type	main, %function
main:
	@ args = 0, pretend = 0, frame = 32
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #32
	mov	r3, #0
	str	r3, [fp, #-8]
	mov	r3, #0
	str	r3, [fp, #-36]
	mov	r3, #0
	str	r3, [fp, #-32]
	mov	r3, #0
	str	r3, [fp, #-28]
	mov	r3, #0
	str	r3, [fp, #-24]
	mov	r3, #0
	str	r3, [fp, #-20]
	mov	r3, #0
	str	r3, [fp, #-16]
	mov	r3, #0
	str	r3, [fp, #-12]
	bl	__VERIFIER_nondet_int
	mov	r3, r0
	str	r3, [fp, #-8]
	ldr	r3, .L21
	ldr	r3, [r3]
	mov	r2, r3
	ldr	r3, [fp, #-8]
	cmp	r3, r2
	bls	.L13
	mov	r3, #0
	b	.L12
.L20:
	ldr	r1, [fp, #-24]
	ldr	r3, .L21+4
	umull	r2, r3, r1, r3
	lsr	r2, r3, #2
	mov	r3, r2
	lsl	r3, r3, #1
	add	r3, r3, r2
	lsl	r3, r3, #1
	sub	r2, r1, r3
	cmp	r2, #0
	bne	.L14
	ldr	r3, [fp, #-20]
	add	r3, r3, #1
	str	r3, [fp, #-20]
	b	.L15
.L14:
	ldr	r1, [fp, #-24]
	ldr	r3, .L21+8
	umull	r2, r3, r1, r3
	lsr	r2, r3, #2
	mov	r3, r2
	lsl	r3, r3, #2
	add	r3, r3, r2
	sub	r2, r1, r3
	cmp	r2, #0
	bne	.L16
	ldr	r3, [fp, #-16]
	add	r3, r3, #1
	str	r3, [fp, #-16]
	b	.L15
.L16:
	ldr	r3, [fp, #-24]
	and	r3, r3, #3
	cmp	r3, #0
	bne	.L17
	ldr	r3, [fp, #-12]
	add	r3, r3, #1
	str	r3, [fp, #-12]
	b	.L15
.L17:
	ldr	r1, [fp, #-24]
	ldr	r3, .L21+4
	umull	r2, r3, r1, r3
	lsr	r2, r3, #1
	mov	r3, r2
	lsl	r3, r3, #1
	add	r3, r3, r2
	sub	r2, r1, r3
	cmp	r2, #0
	bne	.L18
	ldr	r3, [fp, #-36]
	add	r3, r3, #1
	str	r3, [fp, #-36]
	b	.L15
.L18:
	ldr	r3, [fp, #-24]
	and	r3, r3, #1
	cmp	r3, #0
	bne	.L19
	ldr	r3, [fp, #-28]
	add	r3, r3, #1
	str	r3, [fp, #-28]
	b	.L15
.L19:
	ldr	r3, [fp, #-32]
	add	r3, r3, #1
	str	r3, [fp, #-32]
.L15:
	ldr	r3, [fp, #-24]
	add	r3, r3, #1
	str	r3, [fp, #-24]
.L13:
	ldr	r2, [fp, #-24]
	ldr	r3, [fp, #-8]
	cmp	r2, r3
	bcc	.L20
	ldr	r2, [fp, #-36]
	ldr	r3, [fp, #-28]
	add	r2, r2, r3
	ldr	r3, [fp, #-32]
	add	r2, r2, r3
	ldr	r3, [fp, #-12]
	add	r2, r2, r3
	ldr	r3, [fp, #-16]
	add	r2, r2, r3
	ldr	r3, [fp, #-20]
	add	r3, r2, r3
	ldr	r2, [fp, #-24]
	cmp	r2, r3
	moveq	r3, #1
	movne	r3, #0
	and	r3, r3, #255
	mov	r0, r3
	bl	__VERIFIER_assert
	mov	r3, #0
.L12:
	mov	r0, r3
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
.L22:
	.align	2
.L21:
	.word	SIZE
	.word	-1431655765
	.word	-858993459
	.size	main, .-main
	.ident	"GCC: (Ubuntu 9.4.0-1ubuntu1~20.04.2) 9.4.0"
	.section	.note.GNU-stack,"",%progbits
