	.file	"7950451.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	main
	.type	main, @function
main:
.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, 32
	call	__VERIFIER_nondet_double@PLT
	movq	rax, xmm0
	mov	QWORD PTR -8[rbp], rax
	movsd	xmm0, QWORD PTR -8[rbp]
	movsd	QWORD PTR -24[rbp], xmm0
	movsd	xmm0, QWORD PTR .LC0[rip]
	movsd	QWORD PTR -16[rbp], xmm0
	mov	DWORD PTR -28[rbp], 1
.L9:
	movsd	xmm1, QWORD PTR -16[rbp]
	movsd	xmm0, QWORD PTR .LC1[rip]
	mulsd	xmm0, xmm1
	cvttsd2si	ecx, xmm0
	mov	eax, DWORD PTR -28[rbp]
	imul	eax, eax
	mov	edx, eax
	mov	eax, edx
	sal	edx, 2
	sub	eax, edx
	sal	eax, 2
	add	eax, ecx
	cmp	eax, 1
	sete	al
	movzx	eax, al
	mov	edi, eax
	call	__VERIFIER_assert
	mov	eax, DWORD PTR -28[rbp]
	imul	eax, eax
	imul	eax, DWORD PTR -28[rbp]
	lea	ecx, 0[0+rax*4]
	mov	eax, DWORD PTR -28[rbp]
	imul	eax, eax
	mov	edx, eax
	mov	eax, edx
	sal	edx, 2
	sub	eax, edx
	add	eax, eax
	add	ecx, eax
	mov	edx, DWORD PTR -28[rbp]
	mov	eax, edx
	add	eax, eax
	add	eax, edx
	lea	edx, [rcx+rax]
	movsd	xmm1, QWORD PTR -24[rbp]
	movsd	xmm0, QWORD PTR .LC1[rip]
	mulsd	xmm0, xmm1
	movsd	xmm2, QWORD PTR -8[rbp]
	movsd	xmm1, QWORD PTR .LC1[rip]
	mulsd	xmm1, xmm2
	subsd	xmm0, xmm1
	cvttsd2si	eax, xmm0
	add	eax, edx
	cmp	eax, 1
	sete	al
	movzx	eax, al
	mov	edi, eax
	call	__VERIFIER_assert
	mov	eax, DWORD PTR -28[rbp]
	sal	eax, 3
	pxor	xmm0, xmm0
	cvtsi2sd	xmm0, eax
	mulsd	xmm0, QWORD PTR -16[rbp]
	movsd	xmm2, QWORD PTR -8[rbp]
	movsd	xmm1, QWORD PTR .LC2[rip]
	mulsd	xmm2, xmm1
	movapd	xmm1, xmm0
	subsd	xmm1, xmm2
	mov	eax, DWORD PTR -28[rbp]
	sal	eax, 4
	pxor	xmm0, xmm0
	cvtsi2sd	xmm0, eax
	addsd	xmm0, xmm1
	movsd	xmm2, QWORD PTR -16[rbp]
	movsd	xmm1, QWORD PTR .LC3[rip]
	mulsd	xmm2, xmm1
	movapd	xmm1, xmm0
	subsd	xmm1, xmm2
	movsd	xmm2, QWORD PTR -24[rbp]
	movsd	xmm0, QWORD PTR .LC2[rip]
	mulsd	xmm0, xmm2
	addsd	xmm0, xmm1
	movsd	xmm1, QWORD PTR .LC4[rip]
	subsd	xmm0, xmm1
	pxor	xmm1, xmm1
	ucomisd	xmm0, xmm1
	setnp	al
	mov	edx, 0
	pxor	xmm1, xmm1
	ucomisd	xmm0, xmm1
	cmovne	eax, edx
	movzx	eax, al
	mov	edi, eax
	call	__VERIFIER_assert
	movsd	xmm0, QWORD PTR -24[rbp]
	subsd	xmm0, QWORD PTR -16[rbp]
	pxor	xmm1, xmm1
	comisd	xmm0, xmm1
	seta	al
	xor	eax, 1
	test	al, al
	jne	.L12
	movsd	xmm0, QWORD PTR -24[rbp]
	subsd	xmm0, QWORD PTR -16[rbp]
	movsd	QWORD PTR -24[rbp], xmm0
	mov	edx, DWORD PTR -28[rbp]
	mov	eax, edx
	add	eax, eax
	add	eax, edx
	add	eax, eax
	pxor	xmm0, xmm0
	cvtsi2sd	xmm0, eax
	movapd	xmm1, xmm0
	addsd	xmm1, QWORD PTR -16[rbp]
	movsd	xmm0, QWORD PTR .LC4[rip]
	addsd	xmm0, xmm1
	movsd	QWORD PTR -16[rbp], xmm0
	add	DWORD PTR -28[rbp], 1
	jmp	.L9
.L12:
	nop
	movsd	xmm1, QWORD PTR -16[rbp]
	movsd	xmm0, QWORD PTR .LC1[rip]
	mulsd	xmm0, xmm1
	cvttsd2si	ecx, xmm0
	mov	eax, DWORD PTR -28[rbp]
	imul	eax, eax
	mov	edx, eax
	mov	eax, edx
	sal	edx, 2
	sub	eax, edx
	sal	eax, 2
	add	eax, ecx
	cmp	eax, 1
	sete	al
	movzx	eax, al
	mov	edi, eax
	call	__VERIFIER_assert
	mov	eax, DWORD PTR -28[rbp]
	imul	eax, eax
	imul	eax, DWORD PTR -28[rbp]
	lea	ecx, 0[0+rax*4]
	mov	eax, DWORD PTR -28[rbp]
	imul	eax, eax
	mov	edx, eax
	mov	eax, edx
	sal	edx, 2
	sub	eax, edx
	add	eax, eax
	add	ecx, eax
	mov	edx, DWORD PTR -28[rbp]
	mov	eax, edx
	add	eax, eax
	add	eax, edx
	lea	edx, [rcx+rax]
	movsd	xmm1, QWORD PTR -24[rbp]
	movsd	xmm0, QWORD PTR .LC1[rip]
	mulsd	xmm0, xmm1
	movsd	xmm2, QWORD PTR -8[rbp]
	movsd	xmm1, QWORD PTR .LC1[rip]
	mulsd	xmm1, xmm2
	subsd	xmm0, xmm1
	cvttsd2si	eax, xmm0
	add	eax, edx
	cmp	eax, 1
	sete	al
	movzx	eax, al
	mov	edi, eax
	call	__VERIFIER_assert
	mov	eax, DWORD PTR -28[rbp]
	sal	eax, 3
	pxor	xmm0, xmm0
	cvtsi2sd	xmm0, eax
	mulsd	xmm0, QWORD PTR -16[rbp]
	movsd	xmm2, QWORD PTR -8[rbp]
	movsd	xmm1, QWORD PTR .LC2[rip]
	mulsd	xmm2, xmm1
	movapd	xmm1, xmm0
	subsd	xmm1, xmm2
	mov	eax, DWORD PTR -28[rbp]
	sal	eax, 4
	pxor	xmm0, xmm0
	cvtsi2sd	xmm0, eax
	addsd	xmm0, xmm1
	movsd	xmm2, QWORD PTR -16[rbp]
	movsd	xmm1, QWORD PTR .LC3[rip]
	mulsd	xmm2, xmm1
	movapd	xmm1, xmm0
	subsd	xmm1, xmm2
	movsd	xmm2, QWORD PTR -24[rbp]
	movsd	xmm0, QWORD PTR .LC2[rip]
	mulsd	xmm0, xmm2
	addsd	xmm0, xmm1
	movsd	xmm1, QWORD PTR .LC4[rip]
	subsd	xmm0, xmm1
	pxor	xmm1, xmm1
	ucomisd	xmm0, xmm1
	setnp	al
	mov	edx, 0
	pxor	xmm1, xmm1
	ucomisd	xmm0, xmm1
	cmovne	eax, edx
	movzx	eax, al
	mov	edi, eax
	call	__VERIFIER_assert
	mov	eax, 0
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE1:
	.size	main, .-main
	.section	.rodata
	.align 8
.LC0:
	.long	0
	.long	1074397184
	.align 8
.LC1:
	.long	0
	.long	1074790400
	.align 8
.LC2:
	.long	0
	.long	1077411840
	.align 8
.LC3:
	.long	0
	.long	1076363264
	.align 8
.LC4:
	.long	0
	.long	1074266112
	.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	"7950451.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
	.global	__aeabi_dmul
	.global	__aeabi_d2iz
	.global	__aeabi_dsub
	.global	__aeabi_i2d
	.global	__aeabi_dadd
	.global	__aeabi_dcmpeq
	.global	__aeabi_dcmpgt
	.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	{r4, r5, r6, r7, fp, lr}
	add	fp, sp, #20
	sub	sp, sp, #32
	bl	__VERIFIER_nondet_double
	str	r0, [fp, #-28]
	str	r1, [fp, #-24]
	sub	r3, fp, #28
	ldmia	r3, {r2-r3}
	str	r2, [fp, #-44]
	str	r3, [fp, #-40]
	mov	r2, #0
	ldr	r3, .L16
	str	r2, [fp, #-36]
	str	r3, [fp, #-32]
	mov	r3, #1
	str	r3, [fp, #-48]
.L11:
	mov	r2, #0
	ldr	r3, .L16+4
	sub	r1, fp, #36
	ldmia	r1, {r0-r1}
	bl	__aeabi_dmul
	mov	r2, r0
	mov	r3, r1
	mov	r0, r2
	mov	r1, r3
	bl	__aeabi_d2iz
	mov	r1, r0
	ldr	r3, [fp, #-48]
	mul	r2, r3, r3
	mov	r3, r2
	lsl	r2, r2, #2
	sub	r3, r3, r2
	lsl	r3, r3, #2
	add	r3, r1, r3
	cmp	r3, #1
	moveq	r3, #1
	movne	r3, #0
	and	r3, r3, #255
	mov	r0, r3
	bl	__VERIFIER_assert
	ldr	r3, [fp, #-48]
	mov	r2, r3
	mul	r2, r3, r2
	mov	r3, r2
	ldr	r2, [fp, #-48]
	mul	r3, r2, r3
	lsl	r1, r3, #2
	ldr	r3, [fp, #-48]
	mul	r2, r3, r3
	mov	r3, r2
	lsl	r2, r2, #2
	sub	r3, r3, r2
	lsl	r3, r3, #1
	add	r1, r1, r3
	ldr	r2, [fp, #-48]
	mov	r3, r2
	lsl	r3, r3, #1
	add	r3, r3, r2
	add	r4, r1, r3
	mov	r2, #0
	ldr	r3, .L16+4
	sub	r1, fp, #44
	ldmia	r1, {r0-r1}
	bl	__aeabi_dmul
	mov	r2, r0
	mov	r3, r1
	mov	r6, r2
	mov	r7, r3
	mov	r2, #0
	ldr	r3, .L16+4
	sub	r1, fp, #28
	ldmia	r1, {r0-r1}
	bl	__aeabi_dmul
	mov	r2, r0
	mov	r3, r1
	mov	r0, r6
	mov	r1, r7
	bl	__aeabi_dsub
	mov	r2, r0
	mov	r3, r1
	mov	r0, r2
	mov	r1, r3
	bl	__aeabi_d2iz
	mov	r3, r0
	add	r3, r4, r3
	cmp	r3, #1
	moveq	r3, #1
	movne	r3, #0
	and	r3, r3, #255
	mov	r0, r3
	bl	__VERIFIER_assert
	ldr	r3, [fp, #-48]
	lsl	r3, r3, #3
	mov	r0, r3
	bl	__aeabi_i2d
	sub	r3, fp, #36
	ldmia	r3, {r2-r3}
	bl	__aeabi_dmul
	mov	r2, r0
	mov	r3, r1
	mov	r4, r2
	mov	r5, r3
	mov	r2, #0
	ldr	r3, .L16+8
	sub	r1, fp, #28
	ldmia	r1, {r0-r1}
	bl	__aeabi_dmul
	mov	r2, r0
	mov	r3, r1
	mov	r0, r4
	mov	r1, r5
	bl	__aeabi_dsub
	mov	r2, r0
	mov	r3, r1
	mov	r4, r2
	mov	r5, r3
	ldr	r3, [fp, #-48]
	lsl	r3, r3, #4
	mov	r0, r3
	bl	__aeabi_i2d
	mov	r2, r0
	mov	r3, r1
	mov	r0, r4
	mov	r1, r5
	bl	__aeabi_dadd
	mov	r2, r0
	mov	r3, r1
	mov	r4, r2
	mov	r5, r3
	mov	r2, #0
	ldr	r3, .L16+12
	sub	r1, fp, #36
	ldmia	r1, {r0-r1}
	bl	__aeabi_dmul
	mov	r2, r0
	mov	r3, r1
	mov	r0, r4
	mov	r1, r5
	bl	__aeabi_dsub
	mov	r2, r0
	mov	r3, r1
	mov	r4, r2
	mov	r5, r3
	mov	r2, #0
	ldr	r3, .L16+8
	sub	r1, fp, #44
	ldmia	r1, {r0-r1}
	bl	__aeabi_dmul
	mov	r2, r0
	mov	r3, r1
	mov	r0, r4
	mov	r1, r5
	bl	__aeabi_dadd
	mov	r2, r0
	mov	r3, r1
	mov	r0, r2
	mov	r1, r3
	mov	r2, #0
	ldr	r3, .L16+16
	bl	__aeabi_dsub
	mov	r2, r0
	mov	r3, r1
	mov	r0, r2
	mov	r1, r3
	mov	r3, #1
	mov	r4, r3
	mov	r2, #0
	mov	r3, #0
	bl	__aeabi_dcmpeq
	mov	r3, r0
	cmp	r3, #0
	bne	.L7
	mov	r3, #0
	mov	r4, r3
.L7:
	and	r3, r4, #255
	mov	r0, r3
	bl	__VERIFIER_assert
	sub	r3, fp, #36
	ldmia	r3, {r2-r3}
	sub	r1, fp, #44
	ldmia	r1, {r0-r1}
	bl	__aeabi_dsub
	mov	r2, r0
	mov	r3, r1
	mov	r0, r2
	mov	r1, r3
	mov	r3, #1
	mov	r4, r3
	mov	r2, #0
	mov	r3, #0
	bl	__aeabi_dcmpgt
	mov	r3, r0
	cmp	r3, #0
	bne	.L8
	mov	r3, #0
	mov	r4, r3
.L8:
	and	r3, r4, #255
	eor	r3, r3, #1
	and	r3, r3, #255
	cmp	r3, #0
	bne	.L15
	sub	r3, fp, #36
	ldmia	r3, {r2-r3}
	sub	r1, fp, #44
	ldmia	r1, {r0-r1}
	bl	__aeabi_dsub
	mov	r2, r0
	mov	r3, r1
	str	r2, [fp, #-44]
	str	r3, [fp, #-40]
	ldr	r2, [fp, #-48]
	mov	r3, r2
	lsl	r3, r3, #1
	add	r3, r3, r2
	lsl	r3, r3, #1
	mov	r0, r3
	bl	__aeabi_i2d
	sub	r3, fp, #36
	ldmia	r3, {r2-r3}
	bl	__aeabi_dadd
	mov	r2, r0
	mov	r3, r1
	mov	r0, r2
	mov	r1, r3
	mov	r2, #0
	ldr	r3, .L16+16
	bl	__aeabi_dadd
	mov	r2, r0
	mov	r3, r1
	str	r2, [fp, #-36]
	str	r3, [fp, #-32]
	ldr	r3, [fp, #-48]
	add	r3, r3, #1
	str	r3, [fp, #-48]
	b	.L11
.L15:
	nop
	mov	r2, #0
	ldr	r3, .L16+4
	sub	r1, fp, #36
	ldmia	r1, {r0-r1}
	bl	__aeabi_dmul
	mov	r2, r0
	mov	r3, r1
	mov	r0, r2
	mov	r1, r3
	bl	__aeabi_d2iz
	mov	r1, r0
	ldr	r3, [fp, #-48]
	mul	r2, r3, r3
	mov	r3, r2
	lsl	r2, r2, #2
	sub	r3, r3, r2
	lsl	r3, r3, #2
	add	r3, r1, r3
	cmp	r3, #1
	moveq	r3, #1
	movne	r3, #0
	and	r3, r3, #255
	mov	r0, r3
	bl	__VERIFIER_assert
	ldr	r3, [fp, #-48]
	mov	r2, r3
	mul	r2, r3, r2
	mov	r3, r2
	ldr	r2, [fp, #-48]
	mul	r3, r2, r3
	lsl	r1, r3, #2
	ldr	r3, [fp, #-48]
	mul	r2, r3, r3
	mov	r3, r2
	lsl	r2, r2, #2
	sub	r3, r3, r2
	lsl	r3, r3, #1
	add	r1, r1, r3
	ldr	r2, [fp, #-48]
	mov	r3, r2
	lsl	r3, r3, #1
	add	r3, r3, r2
	add	r4, r1, r3
	mov	r2, #0
	ldr	r3, .L16+4
	sub	r1, fp, #44
	ldmia	r1, {r0-r1}
	bl	__aeabi_dmul
	mov	r2, r0
	mov	r3, r1
	mov	r6, r2
	mov	r7, r3
	mov	r2, #0
	ldr	r3, .L16+4
	sub	r1, fp, #28
	ldmia	r1, {r0-r1}
	bl	__aeabi_dmul
	mov	r2, r0
	mov	r3, r1
	mov	r0, r6
	mov	r1, r7
	bl	__aeabi_dsub
	mov	r2, r0
	mov	r3, r1
	mov	r0, r2
	mov	r1, r3
	bl	__aeabi_d2iz
	mov	r3, r0
	add	r3, r4, r3
	cmp	r3, #1
	moveq	r3, #1
	movne	r3, #0
	and	r3, r3, #255
	mov	r0, r3
	bl	__VERIFIER_assert
	ldr	r3, [fp, #-48]
	lsl	r3, r3, #3
	mov	r0, r3
	bl	__aeabi_i2d
	sub	r3, fp, #36
	ldmia	r3, {r2-r3}
	bl	__aeabi_dmul
	mov	r2, r0
	mov	r3, r1
	mov	r4, r2
	mov	r5, r3
	mov	r2, #0
	ldr	r3, .L16+8
	sub	r1, fp, #28
	ldmia	r1, {r0-r1}
	bl	__aeabi_dmul
	mov	r2, r0
	mov	r3, r1
	mov	r0, r4
	mov	r1, r5
	bl	__aeabi_dsub
	mov	r2, r0
	mov	r3, r1
	mov	r4, r2
	mov	r5, r3
	ldr	r3, [fp, #-48]
	lsl	r3, r3, #4
	mov	r0, r3
	bl	__aeabi_i2d
	mov	r2, r0
	mov	r3, r1
	mov	r0, r4
	mov	r1, r5
	bl	__aeabi_dadd
	mov	r2, r0
	mov	r3, r1
	mov	r4, r2
	mov	r5, r3
	mov	r2, #0
	ldr	r3, .L16+12
	sub	r1, fp, #36
	ldmia	r1, {r0-r1}
	bl	__aeabi_dmul
	mov	r2, r0
	mov	r3, r1
	mov	r0, r4
	mov	r1, r5
	bl	__aeabi_dsub
	mov	r2, r0
	mov	r3, r1
	mov	r4, r2
	mov	r5, r3
	mov	r2, #0
	ldr	r3, .L16+8
	sub	r1, fp, #44
	ldmia	r1, {r0-r1}
	bl	__aeabi_dmul
	mov	r2, r0
	mov	r3, r1
	mov	r0, r4
	mov	r1, r5
	bl	__aeabi_dadd
	mov	r2, r0
	mov	r3, r1
	mov	r0, r2
	mov	r1, r3
	mov	r2, #0
	ldr	r3, .L16+16
	bl	__aeabi_dsub
	mov	r2, r0
	mov	r3, r1
	mov	r0, r2
	mov	r1, r3
	mov	r3, #1
	mov	r4, r3
	mov	r2, #0
	mov	r3, #0
	bl	__aeabi_dcmpeq
	mov	r3, r0
	cmp	r3, #0
	bne	.L12
	mov	r3, #0
	mov	r4, r3
.L12:
	and	r3, r4, #255
	mov	r0, r3
	bl	__VERIFIER_assert
	mov	r3, #0
	mov	r0, r3
	sub	sp, fp, #20
	@ sp needed
	pop	{r4, r5, r6, r7, fp, pc}
.L17:
	.align	2
.L16:
	.word	1074397184
	.word	1074790400
	.word	1077411840
	.word	1076363264
	.word	1074266112
	.size	main, .-main
	.ident	"GCC: (Ubuntu 9.4.0-1ubuntu1~20.04.2) 9.4.0"
	.section	.note.GNU-stack,"",%progbits
