	.file	"176905.c"
	.intel_syntax noprefix
	.text
	.globl	__automaton_fail
	.type	__automaton_fail, @function
__automaton_fail:
.LFB0:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
.L2:
	mov	eax, 0
	call	__VERIFIER_error@PLT
	.cfi_endproc
.LFE0:
	.size	__automaton_fail, .-__automaton_fail
	.globl	test
	.type	test, @function
test:
.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
	mov	DWORD PTR -20[rbp], 0
.L4:
	cmp	DWORD PTR -20[rbp], 3
	jg	.L12
	call	__VERIFIER_nondet_int@PLT
	mov	DWORD PTR -16[rbp], eax
	cmp	DWORD PTR -16[rbp], 0
	je	.L7
	call	waterRise
.L7:
	call	__VERIFIER_nondet_int@PLT
	mov	DWORD PTR -12[rbp], eax
	cmp	DWORD PTR -12[rbp], 0
	je	.L8
	call	changeMethaneLevel
.L8:
	call	__VERIFIER_nondet_int@PLT
	mov	DWORD PTR -8[rbp], eax
	cmp	DWORD PTR -8[rbp], 0
	jne	.L9
	call	__VERIFIER_nondet_int@PLT
	mov	DWORD PTR -4[rbp], eax
.L9:
	call	timeShift
	jmp	.L4
.L12:
	nop
.L6:
	call	cleanup
	nop
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE1:
	.size	test, .-test
	.globl	pumpRunning
	.bss
	.align 4
	.type	pumpRunning, @object
	.size	pumpRunning, 4
pumpRunning:
	.zero	4
	.globl	systemActive
	.data
	.align 4
	.type	systemActive, @object
	.size	systemActive, 4
systemActive:
	.long	1
	.text
	.globl	timeShift
	.type	timeShift, @function
timeShift:
.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 pumpRunning[rip]
	test	eax, eax
	je	.L14
	call	lowerWaterLevel
.L14:
	mov	eax, DWORD PTR systemActive[rip]
	test	eax, eax
	je	.L15
	call	processEnvironment
.L15:
	call	__utac_acc__Specification4_spec__1
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE2:
	.size	timeShift, .-timeShift
	.globl	processEnvironment__wrappee__base
	.type	processEnvironment__wrappee__base, @function
processEnvironment__wrappee__base:
.LFB3:
	.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
.LFE3:
	.size	processEnvironment__wrappee__base, .-processEnvironment__wrappee__base
	.globl	processEnvironment
	.type	processEnvironment, @function
processEnvironment:
.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	eax, DWORD PTR pumpRunning[rip]
	test	eax, eax
	je	.L20
	call	isLowWaterLevel
	mov	DWORD PTR -4[rbp], eax
	cmp	DWORD PTR -4[rbp], 0
	je	.L21
	call	deactivatePump
	jmp	.L19
.L21:
	call	processEnvironment__wrappee__base
	jmp	.L19
.L20:
	call	processEnvironment__wrappee__base
	nop
.L19:
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE4:
	.size	processEnvironment, .-processEnvironment
	.globl	activatePump__wrappee__lowWaterSensor
	.type	activatePump__wrappee__lowWaterSensor, @function
activatePump__wrappee__lowWaterSensor:
.LFB5:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	mov	DWORD PTR pumpRunning[rip], 1
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE5:
	.size	activatePump__wrappee__lowWaterSensor, .-activatePump__wrappee__lowWaterSensor
	.globl	activatePump
	.type	activatePump, @function
activatePump:
.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
	call	isMethaneAlarm
	mov	DWORD PTR -4[rbp], eax
	cmp	DWORD PTR -4[rbp], 0
	jne	.L29
	call	activatePump__wrappee__lowWaterSensor
	nop
.L29:
	nop
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE6:
	.size	activatePump, .-activatePump
	.globl	deactivatePump
	.type	deactivatePump, @function
deactivatePump:
.LFB7:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	mov	DWORD PTR pumpRunning[rip], 0
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE7:
	.size	deactivatePump, .-deactivatePump
	.globl	isMethaneAlarm
	.type	isMethaneAlarm, @function
isMethaneAlarm:
.LFB8:
	.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
	call	isMethaneLevelCritical
	mov	DWORD PTR -4[rbp], eax
	mov	eax, DWORD PTR -4[rbp]
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE8:
	.size	isMethaneAlarm, .-isMethaneAlarm
	.globl	isPumpRunning
	.type	isPumpRunning, @function
isPumpRunning:
.LFB9:
	.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 pumpRunning[rip]
	mov	DWORD PTR -4[rbp], eax
	mov	eax, DWORD PTR -4[rbp]
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE9:
	.size	isPumpRunning, .-isPumpRunning
	.section	.rodata
.LC0:
	.string	"Pump(System:"
.LC1:
	.string	"On"
.LC2:
	.string	"Off"
.LC3:
	.string	",Pump:"
.LC4:
	.string	") "
	.text
	.globl	printPump
	.type	printPump, @function
printPump:
.LFB10:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	lea	rdi, .LC0[rip]
	mov	eax, 0
	call	printf@PLT
	mov	eax, DWORD PTR systemActive[rip]
	test	eax, eax
	je	.L37
	lea	rdi, .LC1[rip]
	mov	eax, 0
	call	printf@PLT
	jmp	.L38
.L37:
	lea	rdi, .LC2[rip]
	mov	eax, 0
	call	printf@PLT
.L38:
	lea	rdi, .LC3[rip]
	mov	eax, 0
	call	printf@PLT
	mov	eax, DWORD PTR pumpRunning[rip]
	test	eax, eax
	je	.L39
	lea	rdi, .LC1[rip]
	mov	eax, 0
	call	printf@PLT
	jmp	.L40
.L39:
	lea	rdi, .LC2[rip]
	mov	eax, 0
	call	printf@PLT
.L40:
	lea	rdi, .LC4[rip]
	mov	eax, 0
	call	printf@PLT
	call	printEnvironment
	mov	edi, 10
	call	putchar@PLT
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE10:
	.size	printPump, .-printPump
	.globl	isLowWaterLevel
	.type	isLowWaterLevel, @function
isLowWaterLevel:
.LFB11:
	.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
	call	isLowWaterSensorDry
	mov	DWORD PTR -8[rbp], eax
	cmp	DWORD PTR -8[rbp], 0
	je	.L43
	mov	DWORD PTR -12[rbp], 0
	jmp	.L44
.L43:
	mov	DWORD PTR -12[rbp], 1
.L44:
	mov	eax, DWORD PTR -12[rbp]
	mov	DWORD PTR -4[rbp], eax
	mov	eax, DWORD PTR -4[rbp]
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE11:
	.size	isLowWaterLevel, .-isLowWaterLevel
	.globl	select_one
	.type	select_one, @function
select_one:
.LFB12:
	.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
	call	__VERIFIER_nondet_int@PLT
	mov	DWORD PTR -8[rbp], eax
	mov	eax, DWORD PTR -8[rbp]
	mov	DWORD PTR -4[rbp], eax
	mov	eax, DWORD PTR -4[rbp]
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE12:
	.size	select_one, .-select_one
	.globl	select_features
	.type	select_features, @function
select_features:
.LFB13:
	.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
.LFE13:
	.size	select_features, .-select_features
	.globl	select_helpers
	.type	select_helpers, @function
select_helpers:
.LFB14:
	.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
.LFE14:
	.size	select_helpers, .-select_helpers
	.globl	valid_product
	.type	valid_product, @function
valid_product:
.LFB15:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	mov	DWORD PTR -4[rbp], 1
	mov	eax, DWORD PTR -4[rbp]
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE15:
	.size	valid_product, .-valid_product
	.globl	__utac_acc__Specification4_spec__1
	.type	__utac_acc__Specification4_spec__1, @function
__utac_acc__Specification4_spec__1:
.LFB16:
	.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
	call	getWaterLevel
	mov	DWORD PTR -8[rbp], eax
	cmp	DWORD PTR -8[rbp], 0
	jne	.L57
	call	isPumpRunning
	mov	DWORD PTR -4[rbp], eax
	cmp	DWORD PTR -4[rbp], 0
	je	.L57
	call	__automaton_fail
	nop
.L57:
	nop
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE16:
	.size	__utac_acc__Specification4_spec__1, .-__utac_acc__Specification4_spec__1
	.globl	waterLevel
	.data
	.align 4
	.type	waterLevel, @object
	.size	waterLevel, 4
waterLevel:
	.long	1
	.globl	methaneLevelCritical
	.bss
	.align 4
	.type	methaneLevelCritical, @object
	.size	methaneLevelCritical, 4
methaneLevelCritical:
	.zero	4
	.text
	.globl	lowerWaterLevel
	.type	lowerWaterLevel, @function
lowerWaterLevel:
.LFB17:
	.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 waterLevel[rip]
	test	eax, eax
	jle	.L61
	mov	eax, DWORD PTR waterLevel[rip]
	sub	eax, 1
	mov	DWORD PTR waterLevel[rip], eax
	nop
.L61:
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE17:
	.size	lowerWaterLevel, .-lowerWaterLevel
	.globl	waterRise
	.type	waterRise, @function
waterRise:
.LFB18:
	.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 waterLevel[rip]
	cmp	eax, 1
	jg	.L65
	mov	eax, DWORD PTR waterLevel[rip]
	add	eax, 1
	mov	DWORD PTR waterLevel[rip], eax
	nop
.L65:
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE18:
	.size	waterRise, .-waterRise
	.globl	changeMethaneLevel
	.type	changeMethaneLevel, @function
changeMethaneLevel:
.LFB19:
	.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 methaneLevelCritical[rip]
	test	eax, eax
	je	.L67
	mov	DWORD PTR methaneLevelCritical[rip], 0
	jmp	.L66
.L67:
	mov	DWORD PTR methaneLevelCritical[rip], 1
	nop
.L66:
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE19:
	.size	changeMethaneLevel, .-changeMethaneLevel
	.globl	isMethaneLevelCritical
	.type	isMethaneLevelCritical, @function
isMethaneLevelCritical:
.LFB20:
	.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 methaneLevelCritical[rip]
	mov	DWORD PTR -4[rbp], eax
	mov	eax, DWORD PTR -4[rbp]
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE20:
	.size	isMethaneLevelCritical, .-isMethaneLevelCritical
	.section	.rodata
.LC5:
	.string	"Env(Water:%i"
.LC6:
	.string	",Meth:"
.LC7:
	.string	"CRIT"
.LC8:
	.string	"OK"
	.text
	.globl	printEnvironment
	.type	printEnvironment, @function
printEnvironment:
.LFB21:
	.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 waterLevel[rip]
	mov	esi, eax
	lea	rdi, .LC5[rip]
	mov	eax, 0
	call	printf@PLT
	lea	rdi, .LC6[rip]
	mov	eax, 0
	call	printf@PLT
	mov	eax, DWORD PTR methaneLevelCritical[rip]
	test	eax, eax
	je	.L73
	lea	rdi, .LC7[rip]
	mov	eax, 0
	call	printf@PLT
	jmp	.L74
.L73:
	lea	rdi, .LC8[rip]
	mov	eax, 0
	call	printf@PLT
.L74:
	mov	edi, 41
	call	putchar@PLT
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE21:
	.size	printEnvironment, .-printEnvironment
	.globl	getWaterLevel
	.type	getWaterLevel, @function
getWaterLevel:
.LFB22:
	.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 waterLevel[rip]
	mov	DWORD PTR -4[rbp], eax
	mov	eax, DWORD PTR -4[rbp]
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE22:
	.size	getWaterLevel, .-getWaterLevel
	.globl	isLowWaterSensorDry
	.type	isLowWaterSensorDry, @function
isLowWaterSensorDry:
.LFB23:
	.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 waterLevel[rip]
	test	eax, eax
	sete	al
	movzx	eax, al
	mov	DWORD PTR -4[rbp], eax
	mov	eax, DWORD PTR -4[rbp]
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE23:
	.size	isLowWaterSensorDry, .-isLowWaterSensorDry
	.globl	__utac__exception__cf_handler_set
	.type	__utac__exception__cf_handler_set, @function
__utac__exception__cf_handler_set:
.LFB24:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	sub	rsp, 160
	mov	QWORD PTR -136[rbp], rdi
	mov	QWORD PTR -144[rbp], rsi
	mov	DWORD PTR -148[rbp], edx
	mov	rax, QWORD PTR -136[rbp]
	mov	QWORD PTR -128[rbp], rax
	mov	edi, 24
	call	malloc@PLT
	mov	QWORD PTR -120[rbp], rax
	mov	rax, QWORD PTR -120[rbp]
	mov	QWORD PTR -112[rbp], rax
	mov	rax, QWORD PTR -112[rbp]
	mov	QWORD PTR -104[rbp], rax
	mov	rax, QWORD PTR -104[rbp]
	mov	rdx, QWORD PTR -144[rbp]
	mov	QWORD PTR [rax], rdx
	mov	rax, QWORD PTR -112[rbp]
	mov	QWORD PTR -96[rbp], rax
	mov	rax, QWORD PTR -96[rbp]
	add	rax, 8
	mov	QWORD PTR -88[rbp], rax
	mov	rax, QWORD PTR -88[rbp]
	mov	QWORD PTR -80[rbp], rax
	mov	rax, QWORD PTR -80[rbp]
	mov	edx, DWORD PTR -148[rbp]
	mov	DWORD PTR [rax], edx
	mov	rax, QWORD PTR -112[rbp]
	mov	QWORD PTR -72[rbp], rax
	mov	rax, QWORD PTR -72[rbp]
	add	rax, 16
	mov	QWORD PTR -64[rbp], rax
	mov	rax, QWORD PTR -128[rbp]
	mov	QWORD PTR -56[rbp], rax
	mov	rax, QWORD PTR -56[rbp]
	add	rax, 24
	mov	QWORD PTR -48[rbp], rax
	mov	rax, QWORD PTR -64[rbp]
	mov	QWORD PTR -40[rbp], rax
	mov	rax, QWORD PTR -48[rbp]
	mov	QWORD PTR -32[rbp], rax
	mov	rax, QWORD PTR -32[rbp]
	mov	rdx, QWORD PTR [rax]
	mov	rax, QWORD PTR -40[rbp]
	mov	QWORD PTR [rax], rdx
	mov	rax, QWORD PTR -128[rbp]
	mov	QWORD PTR -24[rbp], rax
	mov	rax, QWORD PTR -24[rbp]
	add	rax, 24
	mov	QWORD PTR -16[rbp], rax
	mov	rax, QWORD PTR -16[rbp]
	mov	QWORD PTR -8[rbp], rax
	mov	rax, QWORD PTR -8[rbp]
	mov	rdx, QWORD PTR -112[rbp]
	mov	QWORD PTR [rax], rdx
	nop
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE24:
	.size	__utac__exception__cf_handler_set, .-__utac__exception__cf_handler_set
	.globl	__utac__exception__cf_handler_free
	.type	__utac__exception__cf_handler_free, @function
__utac__exception__cf_handler_free:
.LFB25:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	sub	rsp, 144
	mov	QWORD PTR -136[rbp], rdi
	mov	rax, QWORD PTR -136[rbp]
	mov	QWORD PTR -120[rbp], rax
	mov	rax, QWORD PTR -120[rbp]
	mov	QWORD PTR -112[rbp], rax
	mov	rax, QWORD PTR -112[rbp]
	add	rax, 24
	mov	QWORD PTR -104[rbp], rax
	mov	rax, QWORD PTR -104[rbp]
	mov	QWORD PTR -96[rbp], rax
	mov	rax, QWORD PTR -96[rbp]
	mov	rax, QWORD PTR [rax]
	mov	QWORD PTR -128[rbp], rax
.L83:
	mov	QWORD PTR -88[rbp], 0
	mov	rax, QWORD PTR -88[rbp]
	mov	QWORD PTR -80[rbp], rax
	mov	rax, QWORD PTR -128[rbp]
	mov	QWORD PTR -72[rbp], rax
	mov	rax, QWORD PTR -72[rbp]
	cmp	rax, QWORD PTR -80[rbp]
	je	.L88
	mov	rax, QWORD PTR -128[rbp]
	mov	QWORD PTR -40[rbp], rax
	mov	rax, QWORD PTR -128[rbp]
	mov	QWORD PTR -32[rbp], rax
	mov	rax, QWORD PTR -32[rbp]
	add	rax, 16
	mov	QWORD PTR -24[rbp], rax
	mov	rax, QWORD PTR -24[rbp]
	mov	QWORD PTR -16[rbp], rax
	mov	rax, QWORD PTR -16[rbp]
	mov	rax, QWORD PTR [rax]
	mov	QWORD PTR -128[rbp], rax
	mov	rax, QWORD PTR -40[rbp]
	mov	QWORD PTR -8[rbp], rax
	mov	rax, QWORD PTR -8[rbp]
	mov	rdi, rax
	call	free@PLT
	jmp	.L83
.L88:
	nop
.L85:
	mov	rax, QWORD PTR -120[rbp]
	mov	QWORD PTR -64[rbp], rax
	mov	rax, QWORD PTR -64[rbp]
	add	rax, 24
	mov	QWORD PTR -56[rbp], rax
	mov	rax, QWORD PTR -56[rbp]
	mov	QWORD PTR -48[rbp], rax
	mov	rax, QWORD PTR -48[rbp]
	mov	QWORD PTR [rax], 0
	nop
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE25:
	.size	__utac__exception__cf_handler_free, .-__utac__exception__cf_handler_free
	.globl	__utac__exception__cf_handler_reset
	.type	__utac__exception__cf_handler_reset, @function
__utac__exception__cf_handler_reset:
.LFB26:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	sub	rsp, 160
	mov	QWORD PTR -152[rbp], rdi
	mov	rax, QWORD PTR -152[rbp]
	mov	QWORD PTR -120[rbp], rax
	mov	rax, QWORD PTR -120[rbp]
	mov	QWORD PTR -112[rbp], rax
	mov	rax, QWORD PTR -112[rbp]
	add	rax, 24
	mov	QWORD PTR -104[rbp], rax
	mov	rax, QWORD PTR -104[rbp]
	mov	QWORD PTR -96[rbp], rax
	mov	rax, QWORD PTR -96[rbp]
	mov	rax, QWORD PTR [rax]
	mov	QWORD PTR -128[rbp], rax
.L90:
	mov	QWORD PTR -88[rbp], 0
	mov	rax, QWORD PTR -88[rbp]
	mov	QWORD PTR -80[rbp], rax
	mov	rax, QWORD PTR -128[rbp]
	mov	QWORD PTR -72[rbp], rax
	mov	rax, QWORD PTR -72[rbp]
	cmp	rax, QWORD PTR -80[rbp]
	je	.L95
	mov	rax, QWORD PTR -128[rbp]
	mov	QWORD PTR -64[rbp], rax
	mov	rax, QWORD PTR -64[rbp]
	mov	rax, QWORD PTR [rax]
	mov	QWORD PTR -56[rbp], rax
	mov	rax, QWORD PTR -128[rbp]
	mov	QWORD PTR -48[rbp], rax
	mov	rax, QWORD PTR -48[rbp]
	add	rax, 8
	mov	QWORD PTR -40[rbp], rax
	mov	rax, QWORD PTR -40[rbp]
	mov	QWORD PTR -32[rbp], rax
	mov	rax, QWORD PTR -32[rbp]
	mov	eax, DWORD PTR [rax]
	mov	DWORD PTR -132[rbp], eax
	mov	eax, DWORD PTR -132[rbp]
	mov	rdx, QWORD PTR -56[rbp]
	mov	esi, eax
	mov	edi, 4
	call	rdx
	mov	rax, QWORD PTR -128[rbp]
	mov	QWORD PTR -24[rbp], rax
	mov	rax, QWORD PTR -24[rbp]
	add	rax, 16
	mov	QWORD PTR -16[rbp], rax
	mov	rax, QWORD PTR -16[rbp]
	mov	QWORD PTR -8[rbp], rax
	mov	rax, QWORD PTR -8[rbp]
	mov	rax, QWORD PTR [rax]
	mov	QWORD PTR -128[rbp], rax
	jmp	.L90
.L95:
	nop
.L92:
	mov	rax, QWORD PTR -152[rbp]
	mov	rdi, rax
	call	__utac__exception__cf_handler_free
	nop
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE26:
	.size	__utac__exception__cf_handler_reset, .-__utac__exception__cf_handler_reset
	.local	head
	.comm	head,8,8
	.globl	__utac__error_stack_mgt
	.type	__utac__error_stack_mgt, @function
__utac__error_stack_mgt:
.LFB27:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	sub	rsp, 192
	mov	QWORD PTR -184[rbp], rdi
	mov	DWORD PTR -188[rbp], esi
	mov	DWORD PTR -192[rbp], edx
	cmp	DWORD PTR -192[rbp], 0
	jne	.L97
	mov	rax, QWORD PTR -160[rbp]
	jmp	.L98
.L97:
	cmp	DWORD PTR -188[rbp], 0
	jne	.L99
	mov	edi, 16
	call	malloc@PLT
	mov	QWORD PTR -48[rbp], rax
	mov	rax, QWORD PTR -48[rbp]
	mov	QWORD PTR -40[rbp], rax
	mov	rax, QWORD PTR -40[rbp]
	mov	QWORD PTR -32[rbp], rax
	mov	rax, QWORD PTR -32[rbp]
	mov	rdx, QWORD PTR -184[rbp]
	mov	QWORD PTR [rax], rdx
	mov	rax, QWORD PTR -40[rbp]
	mov	QWORD PTR -24[rbp], rax
	mov	rax, QWORD PTR -24[rbp]
	add	rax, 8
	mov	QWORD PTR -16[rbp], rax
	mov	rax, QWORD PTR -16[rbp]
	mov	QWORD PTR -8[rbp], rax
	mov	rdx, QWORD PTR head[rip]
	mov	rax, QWORD PTR -8[rbp]
	mov	QWORD PTR [rax], rdx
	mov	rax, QWORD PTR -40[rbp]
	mov	QWORD PTR head[rip], rax
	mov	rax, QWORD PTR -40[rbp]
	mov	QWORD PTR -160[rbp], rax
	mov	rax, QWORD PTR -160[rbp]
	jmp	.L98
.L99:
	cmp	DWORD PTR -188[rbp], 1
	jne	.L100
	mov	rax, QWORD PTR head[rip]
	mov	QWORD PTR -168[rbp], rax
.L101:
	cmp	DWORD PTR -192[rbp], 1
	jle	.L107
	mov	rax, QWORD PTR -168[rbp]
	mov	QWORD PTR -96[rbp], rax
	mov	rax, QWORD PTR -96[rbp]
	add	rax, 8
	mov	QWORD PTR -88[rbp], rax
	mov	rax, QWORD PTR -88[rbp]
	mov	QWORD PTR -80[rbp], rax
	mov	rax, QWORD PTR -80[rbp]
	mov	rax, QWORD PTR [rax]
	mov	QWORD PTR -72[rbp], rax
	mov	rax, QWORD PTR -168[rbp]
	mov	QWORD PTR -64[rbp], rax
	mov	rax, QWORD PTR -64[rbp]
	mov	rax, QWORD PTR [rax]
	mov	QWORD PTR -112[rbp], rax
	mov	rax, QWORD PTR -168[rbp]
	mov	QWORD PTR -56[rbp], rax
	mov	rax, QWORD PTR -56[rbp]
	mov	rdi, rax
	call	free@PLT
	mov	rax, QWORD PTR -112[rbp]
	mov	rdi, rax
	call	__utac__exception__cf_handler_reset
	mov	rax, QWORD PTR -72[rbp]
	mov	QWORD PTR -168[rbp], rax
	sub	DWORD PTR -192[rbp], 1
	jmp	.L101
.L107:
	nop
.L103:
	mov	rax, QWORD PTR -168[rbp]
	mov	QWORD PTR -144[rbp], rax
	mov	rax, QWORD PTR -144[rbp]
	add	rax, 8
	mov	QWORD PTR -136[rbp], rax
	mov	rax, QWORD PTR -136[rbp]
	mov	QWORD PTR -128[rbp], rax
	mov	rax, QWORD PTR -128[rbp]
	mov	rax, QWORD PTR [rax]
	mov	QWORD PTR head[rip], rax
	mov	rax, QWORD PTR -168[rbp]
	mov	QWORD PTR -120[rbp], rax
	mov	rax, QWORD PTR -120[rbp]
	mov	rax, QWORD PTR [rax]
	mov	QWORD PTR -112[rbp], rax
	mov	rax, QWORD PTR -168[rbp]
	mov	QWORD PTR -104[rbp], rax
	mov	rax, QWORD PTR -104[rbp]
	mov	rdi, rax
	call	free@PLT
	mov	rax, QWORD PTR -112[rbp]
	mov	rdi, rax
	call	__utac__exception__cf_handler_reset
	mov	rax, QWORD PTR -112[rbp]
	mov	QWORD PTR -160[rbp], rax
	mov	rax, QWORD PTR -160[rbp]
	jmp	.L98
.L100:
	cmp	DWORD PTR -188[rbp], 2
	jne	.L104
	mov	rax, QWORD PTR head[rip]
	test	rax, rax
	je	.L105
	mov	rax, QWORD PTR head[rip]
	mov	QWORD PTR -152[rbp], rax
	mov	rax, QWORD PTR -152[rbp]
	mov	rax, QWORD PTR [rax]
	mov	QWORD PTR -160[rbp], rax
	mov	rax, QWORD PTR -160[rbp]
	jmp	.L98
.L105:
	mov	QWORD PTR -160[rbp], 0
	mov	rax, QWORD PTR -160[rbp]
	jmp	.L98
.L104:
	mov	rax, QWORD PTR -160[rbp]
.L98:
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE27:
	.size	__utac__error_stack_mgt, .-__utac__error_stack_mgt
	.section	.rodata
.LC9:
	.string	"__utac__get_this_arg"
.LC10:
	.string	"libacc.c"
.LC11:
	.string	"i > 0 && i <= this->argsCount"
	.text
	.globl	__utac__get_this_arg
	.type	__utac__get_this_arg, @function
__utac__get_this_arg:
.LFB28:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	sub	rsp, 96
	mov	DWORD PTR -84[rbp], edi
	mov	QWORD PTR -96[rbp], rsi
	cmp	DWORD PTR -84[rbp], 0
	jle	.L109
	mov	rax, QWORD PTR -96[rbp]
	mov	QWORD PTR -72[rbp], rax
	mov	rax, QWORD PTR -72[rbp]
	add	rax, 16
	mov	QWORD PTR -64[rbp], rax
	mov	rax, QWORD PTR -64[rbp]
	mov	QWORD PTR -56[rbp], rax
	mov	rax, QWORD PTR -56[rbp]
	mov	eax, DWORD PTR [rax]
	mov	DWORD PTR -80[rbp], eax
	mov	eax, DWORD PTR -84[rbp]
	cmp	eax, DWORD PTR -80[rbp]
	jle	.L110
	lea	rcx, .LC9[rip]
	mov	edx, 123
	lea	rsi, .LC10[rip]
	lea	rdi, .LC11[rip]
	call	__assert_fail@PLT
.L109:
	lea	rcx, .LC9[rip]
	mov	edx, 123
	lea	rsi, .LC10[rip]
	lea	rdi, .LC11[rip]
	call	__assert_fail@PLT
.L110:
	mov	eax, DWORD PTR -84[rbp]
	sub	eax, 1
	mov	DWORD PTR -76[rbp], eax
	mov	rax, QWORD PTR -96[rbp]
	mov	QWORD PTR -48[rbp], rax
	mov	rax, QWORD PTR -48[rbp]
	add	rax, 8
	mov	QWORD PTR -40[rbp], rax
	mov	rax, QWORD PTR -40[rbp]
	mov	QWORD PTR -32[rbp], rax
	mov	rax, QWORD PTR -32[rbp]
	mov	rax, QWORD PTR [rax]
	mov	QWORD PTR -24[rbp], rax
	mov	eax, DWORD PTR -76[rbp]
	cdqe
	lea	rdx, 0[0+rax*8]
	mov	rax, QWORD PTR -24[rbp]
	add	rax, rdx
	mov	QWORD PTR -16[rbp], rax
	mov	rax, QWORD PTR -16[rbp]
	mov	rax, QWORD PTR [rax]
	mov	QWORD PTR -8[rbp], rax
	mov	rax, QWORD PTR -8[rbp]
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE28:
	.size	__utac__get_this_arg, .-__utac__get_this_arg
	.section	.rodata
.LC12:
	.string	"__utac__get_this_argtype"
	.text
	.globl	__utac__get_this_argtype
	.type	__utac__get_this_argtype, @function
__utac__get_this_argtype:
.LFB29:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	sub	rsp, 96
	mov	DWORD PTR -84[rbp], edi
	mov	QWORD PTR -96[rbp], rsi
	cmp	DWORD PTR -84[rbp], 0
	jle	.L113
	mov	rax, QWORD PTR -96[rbp]
	mov	QWORD PTR -72[rbp], rax
	mov	rax, QWORD PTR -72[rbp]
	add	rax, 16
	mov	QWORD PTR -64[rbp], rax
	mov	rax, QWORD PTR -64[rbp]
	mov	QWORD PTR -56[rbp], rax
	mov	rax, QWORD PTR -56[rbp]
	mov	eax, DWORD PTR [rax]
	mov	DWORD PTR -80[rbp], eax
	mov	eax, DWORD PTR -84[rbp]
	cmp	eax, DWORD PTR -80[rbp]
	jle	.L114
	lea	rcx, .LC12[rip]
	mov	edx, 131
	lea	rsi, .LC10[rip]
	lea	rdi, .LC11[rip]
	call	__assert_fail@PLT
.L113:
	lea	rcx, .LC12[rip]
	mov	edx, 131
	lea	rsi, .LC10[rip]
	lea	rdi, .LC11[rip]
	call	__assert_fail@PLT
.L114:
	mov	eax, DWORD PTR -84[rbp]
	sub	eax, 1
	mov	DWORD PTR -76[rbp], eax
	mov	rax, QWORD PTR -96[rbp]
	mov	QWORD PTR -48[rbp], rax
	mov	rax, QWORD PTR -48[rbp]
	add	rax, 24
	mov	QWORD PTR -40[rbp], rax
	mov	rax, QWORD PTR -40[rbp]
	mov	QWORD PTR -32[rbp], rax
	mov	rax, QWORD PTR -32[rbp]
	mov	rax, QWORD PTR [rax]
	mov	QWORD PTR -24[rbp], rax
	mov	eax, DWORD PTR -76[rbp]
	cdqe
	lea	rdx, 0[0+rax*8]
	mov	rax, QWORD PTR -24[rbp]
	add	rax, rdx
	mov	QWORD PTR -16[rbp], rax
	mov	rax, QWORD PTR -16[rbp]
	mov	rax, QWORD PTR [rax]
	mov	QWORD PTR -8[rbp], rax
	mov	rax, QWORD PTR -8[rbp]
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE29:
	.size	__utac__get_this_argtype, .-__utac__get_this_argtype
	.globl	cleanupTimeShifts
	.data
	.align 4
	.type	cleanupTimeShifts, @object
	.size	cleanupTimeShifts, 4
cleanupTimeShifts:
	.long	4
	.text
	.globl	cleanup
	.type	cleanup, @function
cleanup:
.LFB30:
	.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
	call	timeShift
	mov	DWORD PTR -8[rbp], 0
.L117:
	mov	eax, DWORD PTR cleanupTimeShifts[rip]
	sub	eax, 1
	mov	DWORD PTR -4[rbp], eax
	mov	eax, DWORD PTR -8[rbp]
	cmp	eax, DWORD PTR -4[rbp]
	jge	.L122
	call	timeShift
	add	DWORD PTR -8[rbp], 1
	jmp	.L117
.L122:
	nop
.L119:
	nop
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE30:
	.size	cleanup, .-cleanup
	.globl	Specification2
	.type	Specification2, @function
Specification2:
.LFB31:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	call	timeShift
	call	printPump
	call	timeShift
	call	printPump
	call	timeShift
	call	printPump
	call	waterRise
	call	printPump
	call	timeShift
	call	printPump
	call	changeMethaneLevel
	call	printPump
	call	timeShift
	call	printPump
	call	cleanup
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE31:
	.size	Specification2, .-Specification2
	.globl	setup
	.type	setup, @function
setup:
.LFB32:
	.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
.LFE32:
	.size	setup, .-setup
	.globl	runTest
	.type	runTest, @function
runTest:
.LFB33:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	call	test
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE33:
	.size	runTest, .-runTest
	.globl	main
	.type	main, @function
main:
.LFB34:
	.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
	call	select_helpers
	call	select_features
	call	valid_product
	mov	DWORD PTR -8[rbp], eax
	cmp	DWORD PTR -8[rbp], 0
	je	.L130
	call	setup
	call	runTest
.L130:
	mov	DWORD PTR -4[rbp], 0
	mov	eax, DWORD PTR -4[rbp]
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE34:
	.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	"176905.c"
	.text
	.align	2
	.global	__automaton_fail
	.syntax unified
	.arm
	.fpu softvfp
	.type	__automaton_fail, %function
__automaton_fail:
	@ args = 0, pretend = 0, frame = 0
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
.L2:
	bl	__VERIFIER_error
	.size	__automaton_fail, .-__automaton_fail
	.align	2
	.global	test
	.syntax unified
	.arm
	.fpu softvfp
	.type	test, %function
test:
	@ args = 0, pretend = 0, frame = 24
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #24
	mov	r3, #0
	str	r3, [fp, #-24]
.L4:
	ldr	r3, [fp, #-24]
	cmp	r3, #3
	bgt	.L12
	bl	__VERIFIER_nondet_int
	str	r0, [fp, #-20]
	ldr	r3, [fp, #-20]
	cmp	r3, #0
	beq	.L7
	bl	waterRise
.L7:
	bl	__VERIFIER_nondet_int
	str	r0, [fp, #-16]
	ldr	r3, [fp, #-16]
	cmp	r3, #0
	beq	.L8
	bl	changeMethaneLevel
.L8:
	bl	__VERIFIER_nondet_int
	str	r0, [fp, #-12]
	ldr	r3, [fp, #-12]
	cmp	r3, #0
	bne	.L9
	bl	__VERIFIER_nondet_int
	str	r0, [fp, #-8]
.L9:
	bl	timeShift
	b	.L4
.L12:
	nop
.L6:
	bl	cleanup
	nop
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
	.size	test, .-test
	.global	pumpRunning
	.bss
	.align	2
	.type	pumpRunning, %object
	.size	pumpRunning, 4
pumpRunning:
	.space	4
	.global	systemActive
	.data
	.align	2
	.type	systemActive, %object
	.size	systemActive, 4
systemActive:
	.word	1
	.text
	.align	2
	.global	timeShift
	.syntax unified
	.arm
	.fpu softvfp
	.type	timeShift, %function
timeShift:
	@ args = 0, pretend = 0, frame = 0
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	ldr	r3, .L17
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L14
	bl	lowerWaterLevel
.L14:
	ldr	r3, .L17+4
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L15
	bl	processEnvironment
.L15:
	bl	__utac_acc__Specification4_spec__1
	nop
	pop	{fp, pc}
.L18:
	.align	2
.L17:
	.word	pumpRunning
	.word	systemActive
	.size	timeShift, .-timeShift
	.align	2
	.global	processEnvironment__wrappee__base
	.syntax unified
	.arm
	.fpu softvfp
	.type	processEnvironment__wrappee__base, %function
processEnvironment__wrappee__base:
	@ 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	processEnvironment__wrappee__base, .-processEnvironment__wrappee__base
	.align	2
	.global	processEnvironment
	.syntax unified
	.arm
	.fpu softvfp
	.type	processEnvironment, %function
processEnvironment:
	@ args = 0, pretend = 0, frame = 8
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #8
	ldr	r3, .L26
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L22
	bl	isLowWaterLevel
	str	r0, [fp, #-8]
	ldr	r3, [fp, #-8]
	cmp	r3, #0
	beq	.L23
	bl	deactivatePump
	b	.L21
.L23:
	bl	processEnvironment__wrappee__base
	b	.L21
.L22:
	bl	processEnvironment__wrappee__base
	nop
.L21:
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
.L27:
	.align	2
.L26:
	.word	pumpRunning
	.size	processEnvironment, .-processEnvironment
	.align	2
	.global	activatePump__wrappee__lowWaterSensor
	.syntax unified
	.arm
	.fpu softvfp
	.type	activatePump__wrappee__lowWaterSensor, %function
activatePump__wrappee__lowWaterSensor:
	@ 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
	ldr	r3, .L30
	mov	r2, #1
	str	r2, [r3]
	nop
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
.L31:
	.align	2
.L30:
	.word	pumpRunning
	.size	activatePump__wrappee__lowWaterSensor, .-activatePump__wrappee__lowWaterSensor
	.align	2
	.global	activatePump
	.syntax unified
	.arm
	.fpu softvfp
	.type	activatePump, %function
activatePump:
	@ args = 0, pretend = 0, frame = 8
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #8
	bl	isMethaneAlarm
	str	r0, [fp, #-8]
	ldr	r3, [fp, #-8]
	cmp	r3, #0
	bne	.L35
	bl	activatePump__wrappee__lowWaterSensor
	nop
.L35:
	nop
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
	.size	activatePump, .-activatePump
	.align	2
	.global	deactivatePump
	.syntax unified
	.arm
	.fpu softvfp
	.type	deactivatePump, %function
deactivatePump:
	@ 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
	ldr	r3, .L38
	mov	r2, #0
	str	r2, [r3]
	nop
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
.L39:
	.align	2
.L38:
	.word	pumpRunning
	.size	deactivatePump, .-deactivatePump
	.align	2
	.global	isMethaneAlarm
	.syntax unified
	.arm
	.fpu softvfp
	.type	isMethaneAlarm, %function
isMethaneAlarm:
	@ args = 0, pretend = 0, frame = 8
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #8
	bl	isMethaneLevelCritical
	str	r0, [fp, #-8]
	ldr	r3, [fp, #-8]
	mov	r0, r3
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
	.size	isMethaneAlarm, .-isMethaneAlarm
	.align	2
	.global	isPumpRunning
	.syntax unified
	.arm
	.fpu softvfp
	.type	isPumpRunning, %function
isPumpRunning:
	@ args = 0, pretend = 0, frame = 8
	@ frame_needed = 1, uses_anonymous_args = 0
	@ link register save eliminated.
	str	fp, [sp, #-4]!
	add	fp, sp, #0
	sub	sp, sp, #12
	ldr	r3, .L44
	ldr	r3, [r3]
	str	r3, [fp, #-8]
	ldr	r3, [fp, #-8]
	mov	r0, r3
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
.L45:
	.align	2
.L44:
	.word	pumpRunning
	.size	isPumpRunning, .-isPumpRunning
	.section	.rodata
	.align	2
.LC0:
	.ascii	"Pump(System:\000"
	.align	2
.LC1:
	.ascii	"On\000"
	.align	2
.LC2:
	.ascii	"Off\000"
	.align	2
.LC3:
	.ascii	",Pump:\000"
	.align	2
.LC4:
	.ascii	") \000"
	.text
	.align	2
	.global	printPump
	.syntax unified
	.arm
	.fpu softvfp
	.type	printPump, %function
printPump:
	@ args = 0, pretend = 0, frame = 0
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	ldr	r0, .L52
	bl	printf
	ldr	r3, .L52+4
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L47
	ldr	r0, .L52+8
	bl	printf
	b	.L48
.L47:
	ldr	r0, .L52+12
	bl	printf
.L48:
	ldr	r0, .L52+16
	bl	printf
	ldr	r3, .L52+20
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L49
	ldr	r0, .L52+8
	bl	printf
	b	.L50
.L49:
	ldr	r0, .L52+12
	bl	printf
.L50:
	ldr	r0, .L52+24
	bl	printf
	bl	printEnvironment
	mov	r0, #10
	bl	putchar
	nop
	pop	{fp, pc}
.L53:
	.align	2
.L52:
	.word	.LC0
	.word	systemActive
	.word	.LC1
	.word	.LC2
	.word	.LC3
	.word	pumpRunning
	.word	.LC4
	.size	printPump, .-printPump
	.align	2
	.global	isLowWaterLevel
	.syntax unified
	.arm
	.fpu softvfp
	.type	isLowWaterLevel, %function
isLowWaterLevel:
	@ args = 0, pretend = 0, frame = 16
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #16
	bl	isLowWaterSensorDry
	str	r0, [fp, #-12]
	ldr	r3, [fp, #-12]
	cmp	r3, #0
	beq	.L55
	mov	r3, #0
	str	r3, [fp, #-16]
	b	.L56
.L55:
	mov	r3, #1
	str	r3, [fp, #-16]
.L56:
	ldr	r3, [fp, #-16]
	str	r3, [fp, #-8]
	ldr	r3, [fp, #-8]
	mov	r0, r3
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
	.size	isLowWaterLevel, .-isLowWaterLevel
	.align	2
	.global	select_one
	.syntax unified
	.arm
	.fpu softvfp
	.type	select_one, %function
select_one:
	@ args = 0, pretend = 0, frame = 8
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #8
	bl	__VERIFIER_nondet_int
	str	r0, [fp, #-12]
	ldr	r3, [fp, #-12]
	str	r3, [fp, #-8]
	ldr	r3, [fp, #-8]
	mov	r0, r3
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
	.size	select_one, .-select_one
	.align	2
	.global	select_features
	.syntax unified
	.arm
	.fpu softvfp
	.type	select_features, %function
select_features:
	@ 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	select_features, .-select_features
	.align	2
	.global	select_helpers
	.syntax unified
	.arm
	.fpu softvfp
	.type	select_helpers, %function
select_helpers:
	@ 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	select_helpers, .-select_helpers
	.align	2
	.global	valid_product
	.syntax unified
	.arm
	.fpu softvfp
	.type	valid_product, %function
valid_product:
	@ args = 0, pretend = 0, frame = 8
	@ frame_needed = 1, uses_anonymous_args = 0
	@ link register save eliminated.
	str	fp, [sp, #-4]!
	add	fp, sp, #0
	sub	sp, sp, #12
	mov	r3, #1
	str	r3, [fp, #-8]
	ldr	r3, [fp, #-8]
	mov	r0, r3
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
	.size	valid_product, .-valid_product
	.align	2
	.global	__utac_acc__Specification4_spec__1
	.syntax unified
	.arm
	.fpu softvfp
	.type	__utac_acc__Specification4_spec__1, %function
__utac_acc__Specification4_spec__1:
	@ args = 0, pretend = 0, frame = 8
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #8
	bl	getWaterLevel
	str	r0, [fp, #-12]
	ldr	r3, [fp, #-12]
	cmp	r3, #0
	bne	.L69
	bl	isPumpRunning
	str	r0, [fp, #-8]
	ldr	r3, [fp, #-8]
	cmp	r3, #0
	beq	.L69
	bl	__automaton_fail
	nop
.L69:
	nop
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
	.size	__utac_acc__Specification4_spec__1, .-__utac_acc__Specification4_spec__1
	.global	waterLevel
	.data
	.align	2
	.type	waterLevel, %object
	.size	waterLevel, 4
waterLevel:
	.word	1
	.global	methaneLevelCritical
	.bss
	.align	2
	.type	methaneLevelCritical, %object
	.size	methaneLevelCritical, 4
methaneLevelCritical:
	.space	4
	.text
	.align	2
	.global	lowerWaterLevel
	.syntax unified
	.arm
	.fpu softvfp
	.type	lowerWaterLevel, %function
lowerWaterLevel:
	@ 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
	ldr	r3, .L74
	ldr	r3, [r3]
	cmp	r3, #0
	ble	.L73
	ldr	r3, .L74
	ldr	r3, [r3]
	sub	r3, r3, #1
	ldr	r2, .L74
	str	r3, [r2]
	nop
.L73:
	nop
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
.L75:
	.align	2
.L74:
	.word	waterLevel
	.size	lowerWaterLevel, .-lowerWaterLevel
	.align	2
	.global	waterRise
	.syntax unified
	.arm
	.fpu softvfp
	.type	waterRise, %function
waterRise:
	@ 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
	ldr	r3, .L80
	ldr	r3, [r3]
	cmp	r3, #1
	bgt	.L79
	ldr	r3, .L80
	ldr	r3, [r3]
	add	r3, r3, #1
	ldr	r2, .L80
	str	r3, [r2]
	nop
.L79:
	nop
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
.L81:
	.align	2
.L80:
	.word	waterLevel
	.size	waterRise, .-waterRise
	.align	2
	.global	changeMethaneLevel
	.syntax unified
	.arm
	.fpu softvfp
	.type	changeMethaneLevel, %function
changeMethaneLevel:
	@ 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
	ldr	r3, .L86
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L83
	ldr	r3, .L86
	mov	r2, #0
	str	r2, [r3]
	b	.L82
.L83:
	ldr	r3, .L86
	mov	r2, #1
	str	r2, [r3]
	nop
.L82:
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
.L87:
	.align	2
.L86:
	.word	methaneLevelCritical
	.size	changeMethaneLevel, .-changeMethaneLevel
	.align	2
	.global	isMethaneLevelCritical
	.syntax unified
	.arm
	.fpu softvfp
	.type	isMethaneLevelCritical, %function
isMethaneLevelCritical:
	@ args = 0, pretend = 0, frame = 8
	@ frame_needed = 1, uses_anonymous_args = 0
	@ link register save eliminated.
	str	fp, [sp, #-4]!
	add	fp, sp, #0
	sub	sp, sp, #12
	ldr	r3, .L90
	ldr	r3, [r3]
	str	r3, [fp, #-8]
	ldr	r3, [fp, #-8]
	mov	r0, r3
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
.L91:
	.align	2
.L90:
	.word	methaneLevelCritical
	.size	isMethaneLevelCritical, .-isMethaneLevelCritical
	.section	.rodata
	.align	2
.LC5:
	.ascii	"Env(Water:%i\000"
	.align	2
.LC6:
	.ascii	",Meth:\000"
	.align	2
.LC7:
	.ascii	"CRIT\000"
	.align	2
.LC8:
	.ascii	"OK\000"
	.text
	.align	2
	.global	printEnvironment
	.syntax unified
	.arm
	.fpu softvfp
	.type	printEnvironment, %function
printEnvironment:
	@ args = 0, pretend = 0, frame = 0
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	ldr	r3, .L96
	ldr	r3, [r3]
	mov	r1, r3
	ldr	r0, .L96+4
	bl	printf
	ldr	r0, .L96+8
	bl	printf
	ldr	r3, .L96+12
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L93
	ldr	r0, .L96+16
	bl	printf
	b	.L94
.L93:
	ldr	r0, .L96+20
	bl	printf
.L94:
	mov	r0, #41
	bl	putchar
	nop
	pop	{fp, pc}
.L97:
	.align	2
.L96:
	.word	waterLevel
	.word	.LC5
	.word	.LC6
	.word	methaneLevelCritical
	.word	.LC7
	.word	.LC8
	.size	printEnvironment, .-printEnvironment
	.align	2
	.global	getWaterLevel
	.syntax unified
	.arm
	.fpu softvfp
	.type	getWaterLevel, %function
getWaterLevel:
	@ args = 0, pretend = 0, frame = 8
	@ frame_needed = 1, uses_anonymous_args = 0
	@ link register save eliminated.
	str	fp, [sp, #-4]!
	add	fp, sp, #0
	sub	sp, sp, #12
	ldr	r3, .L100
	ldr	r3, [r3]
	str	r3, [fp, #-8]
	ldr	r3, [fp, #-8]
	mov	r0, r3
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
.L101:
	.align	2
.L100:
	.word	waterLevel
	.size	getWaterLevel, .-getWaterLevel
	.align	2
	.global	isLowWaterSensorDry
	.syntax unified
	.arm
	.fpu softvfp
	.type	isLowWaterSensorDry, %function
isLowWaterSensorDry:
	@ args = 0, pretend = 0, frame = 8
	@ frame_needed = 1, uses_anonymous_args = 0
	@ link register save eliminated.
	str	fp, [sp, #-4]!
	add	fp, sp, #0
	sub	sp, sp, #12
	ldr	r3, .L104
	ldr	r3, [r3]
	cmp	r3, #0
	moveq	r3, #1
	movne	r3, #0
	and	r3, r3, #255
	str	r3, [fp, #-8]
	ldr	r3, [fp, #-8]
	mov	r0, r3
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
.L105:
	.align	2
.L104:
	.word	waterLevel
	.size	isLowWaterSensorDry, .-isLowWaterSensorDry
	.align	2
	.global	__utac__exception__cf_handler_set
	.syntax unified
	.arm
	.fpu softvfp
	.type	__utac__exception__cf_handler_set, %function
__utac__exception__cf_handler_set:
	@ args = 0, pretend = 0, frame = 80
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #80
	str	r0, [fp, #-72]
	str	r1, [fp, #-76]
	str	r2, [fp, #-80]
	ldr	r3, [fp, #-72]
	str	r3, [fp, #-68]
	mov	r0, #24
	bl	malloc
	mov	r3, r0
	str	r3, [fp, #-64]
	ldr	r3, [fp, #-64]
	str	r3, [fp, #-60]
	ldr	r3, [fp, #-60]
	str	r3, [fp, #-56]
	ldr	r3, [fp, #-56]
	ldr	r2, [fp, #-76]
	str	r2, [r3]
	ldr	r3, [fp, #-60]
	str	r3, [fp, #-52]
	ldr	r3, [fp, #-52]
	add	r3, r3, #8
	str	r3, [fp, #-48]
	ldr	r3, [fp, #-48]
	str	r3, [fp, #-44]
	ldr	r3, [fp, #-44]
	ldr	r2, [fp, #-80]
	str	r2, [r3]
	ldr	r3, [fp, #-60]
	str	r3, [fp, #-40]
	ldr	r3, [fp, #-40]
	add	r3, r3, #16
	str	r3, [fp, #-36]
	ldr	r3, [fp, #-68]
	str	r3, [fp, #-32]
	ldr	r3, [fp, #-32]
	add	r3, r3, #24
	str	r3, [fp, #-28]
	ldr	r3, [fp, #-36]
	str	r3, [fp, #-24]
	ldr	r3, [fp, #-28]
	str	r3, [fp, #-20]
	ldr	r3, [fp, #-20]
	ldr	r2, [r3]
	ldr	r3, [fp, #-24]
	str	r2, [r3]
	ldr	r3, [fp, #-68]
	str	r3, [fp, #-16]
	ldr	r3, [fp, #-16]
	add	r3, r3, #24
	str	r3, [fp, #-12]
	ldr	r3, [fp, #-12]
	str	r3, [fp, #-8]
	ldr	r3, [fp, #-8]
	ldr	r2, [fp, #-60]
	str	r2, [r3]
	nop
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
	.size	__utac__exception__cf_handler_set, .-__utac__exception__cf_handler_set
	.align	2
	.global	__utac__exception__cf_handler_free
	.syntax unified
	.arm
	.fpu softvfp
	.type	__utac__exception__cf_handler_free, %function
__utac__exception__cf_handler_free:
	@ args = 0, pretend = 0, frame = 72
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #72
	str	r0, [fp, #-72]
	ldr	r3, [fp, #-72]
	str	r3, [fp, #-64]
	ldr	r3, [fp, #-64]
	str	r3, [fp, #-60]
	ldr	r3, [fp, #-60]
	add	r3, r3, #24
	str	r3, [fp, #-56]
	ldr	r3, [fp, #-56]
	str	r3, [fp, #-52]
	ldr	r3, [fp, #-52]
	ldr	r3, [r3]
	str	r3, [fp, #-68]
.L109:
	mov	r3, #0
	str	r3, [fp, #-48]
	ldr	r3, [fp, #-48]
	str	r3, [fp, #-44]
	ldr	r3, [fp, #-68]
	str	r3, [fp, #-40]
	ldr	r2, [fp, #-40]
	ldr	r3, [fp, #-44]
	cmp	r2, r3
	beq	.L114
	ldr	r3, [fp, #-68]
	str	r3, [fp, #-24]
	ldr	r3, [fp, #-68]
	str	r3, [fp, #-20]
	ldr	r3, [fp, #-20]
	add	r3, r3, #16
	str	r3, [fp, #-16]
	ldr	r3, [fp, #-16]
	str	r3, [fp, #-12]
	ldr	r3, [fp, #-12]
	ldr	r3, [r3]
	str	r3, [fp, #-68]
	ldr	r3, [fp, #-24]
	str	r3, [fp, #-8]
	ldr	r0, [fp, #-8]
	bl	free
	b	.L109
.L114:
	nop
.L111:
	ldr	r3, [fp, #-64]
	str	r3, [fp, #-36]
	ldr	r3, [fp, #-36]
	add	r3, r3, #24
	str	r3, [fp, #-32]
	ldr	r3, [fp, #-32]
	str	r3, [fp, #-28]
	ldr	r3, [fp, #-28]
	mov	r2, #0
	str	r2, [r3]
	nop
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
	.size	__utac__exception__cf_handler_free, .-__utac__exception__cf_handler_free
	.align	2
	.global	__utac__exception__cf_handler_reset
	.syntax unified
	.arm
	.fpu softvfp
	.type	__utac__exception__cf_handler_reset, %function
__utac__exception__cf_handler_reset:
	@ args = 0, pretend = 0, frame = 80
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #80
	str	r0, [fp, #-80]
	ldr	r3, [fp, #-80]
	str	r3, [fp, #-68]
	ldr	r3, [fp, #-68]
	str	r3, [fp, #-64]
	ldr	r3, [fp, #-64]
	add	r3, r3, #24
	str	r3, [fp, #-60]
	ldr	r3, [fp, #-60]
	str	r3, [fp, #-56]
	ldr	r3, [fp, #-56]
	ldr	r3, [r3]
	str	r3, [fp, #-72]
.L116:
	mov	r3, #0
	str	r3, [fp, #-52]
	ldr	r3, [fp, #-52]
	str	r3, [fp, #-48]
	ldr	r3, [fp, #-72]
	str	r3, [fp, #-44]
	ldr	r2, [fp, #-44]
	ldr	r3, [fp, #-48]
	cmp	r2, r3
	beq	.L121
	ldr	r3, [fp, #-72]
	str	r3, [fp, #-40]
	ldr	r3, [fp, #-40]
	ldr	r3, [r3]
	str	r3, [fp, #-36]
	ldr	r3, [fp, #-72]
	str	r3, [fp, #-32]
	ldr	r3, [fp, #-32]
	add	r3, r3, #8
	str	r3, [fp, #-28]
	ldr	r3, [fp, #-28]
	str	r3, [fp, #-24]
	ldr	r3, [fp, #-24]
	ldr	r3, [r3]
	str	r3, [fp, #-20]
	ldr	r3, [fp, #-36]
	ldr	r1, [fp, #-20]
	mov	r0, #4
	blx	r3
	ldr	r3, [fp, #-72]
	str	r3, [fp, #-16]
	ldr	r3, [fp, #-16]
	add	r3, r3, #16
	str	r3, [fp, #-12]
	ldr	r3, [fp, #-12]
	str	r3, [fp, #-8]
	ldr	r3, [fp, #-8]
	ldr	r3, [r3]
	str	r3, [fp, #-72]
	b	.L116
.L121:
	nop
.L118:
	ldr	r0, [fp, #-80]
	bl	__utac__exception__cf_handler_free
	nop
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
	.size	__utac__exception__cf_handler_reset, .-__utac__exception__cf_handler_reset
	.local	head
	.comm	head,4,4
	.align	2
	.global	__utac__error_stack_mgt
	.syntax unified
	.arm
	.fpu softvfp
	.type	__utac__error_stack_mgt, %function
__utac__error_stack_mgt:
	@ args = 0, pretend = 0, frame = 104
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #104
	str	r0, [fp, #-96]
	str	r1, [fp, #-100]
	str	r2, [fp, #-104]
	ldr	r3, [fp, #-104]
	cmp	r3, #0
	bne	.L123
	ldr	r3, [fp, #-84]
	b	.L124
.L123:
	ldr	r3, [fp, #-100]
	cmp	r3, #0
	bne	.L125
	mov	r0, #16
	bl	malloc
	mov	r3, r0
	str	r3, [fp, #-28]
	ldr	r3, [fp, #-28]
	str	r3, [fp, #-24]
	ldr	r3, [fp, #-24]
	str	r3, [fp, #-20]
	ldr	r3, [fp, #-20]
	ldr	r2, [fp, #-96]
	str	r2, [r3]
	ldr	r3, [fp, #-24]
	str	r3, [fp, #-16]
	ldr	r3, [fp, #-16]
	add	r3, r3, #8
	str	r3, [fp, #-12]
	ldr	r3, [fp, #-12]
	str	r3, [fp, #-8]
	ldr	r3, .L134
	ldr	r2, [r3]
	ldr	r3, [fp, #-8]
	str	r2, [r3]
	ldr	r2, .L134
	ldr	r3, [fp, #-24]
	str	r3, [r2]
	ldr	r3, [fp, #-24]
	str	r3, [fp, #-84]
	ldr	r3, [fp, #-84]
	b	.L124
.L125:
	ldr	r3, [fp, #-100]
	cmp	r3, #1
	bne	.L126
	ldr	r3, .L134
	ldr	r3, [r3]
	str	r3, [fp, #-88]
.L127:
	ldr	r3, [fp, #-104]
	cmp	r3, #1
	ble	.L133
	ldr	r3, [fp, #-88]
	str	r3, [fp, #-52]
	ldr	r3, [fp, #-52]
	add	r3, r3, #8
	str	r3, [fp, #-48]
	ldr	r3, [fp, #-48]
	str	r3, [fp, #-44]
	ldr	r3, [fp, #-44]
	ldr	r3, [r3]
	str	r3, [fp, #-40]
	ldr	r3, [fp, #-88]
	str	r3, [fp, #-36]
	ldr	r3, [fp, #-36]
	ldr	r3, [r3]
	str	r3, [fp, #-60]
	ldr	r3, [fp, #-88]
	str	r3, [fp, #-32]
	ldr	r0, [fp, #-32]
	bl	free
	ldr	r0, [fp, #-60]
	bl	__utac__exception__cf_handler_reset
	ldr	r3, [fp, #-40]
	str	r3, [fp, #-88]
	ldr	r3, [fp, #-104]
	sub	r3, r3, #1
	str	r3, [fp, #-104]
	b	.L127
.L133:
	nop
.L129:
	ldr	r3, [fp, #-88]
	str	r3, [fp, #-76]
	ldr	r3, [fp, #-76]
	add	r3, r3, #8
	str	r3, [fp, #-72]
	ldr	r3, [fp, #-72]
	str	r3, [fp, #-68]
	ldr	r3, [fp, #-68]
	ldr	r3, [r3]
	ldr	r2, .L134
	str	r3, [r2]
	ldr	r3, [fp, #-88]
	str	r3, [fp, #-64]
	ldr	r3, [fp, #-64]
	ldr	r3, [r3]
	str	r3, [fp, #-60]
	ldr	r3, [fp, #-88]
	str	r3, [fp, #-56]
	ldr	r0, [fp, #-56]
	bl	free
	ldr	r0, [fp, #-60]
	bl	__utac__exception__cf_handler_reset
	ldr	r3, [fp, #-60]
	str	r3, [fp, #-84]
	ldr	r3, [fp, #-84]
	b	.L124
.L126:
	ldr	r3, [fp, #-100]
	cmp	r3, #2
	bne	.L130
	ldr	r3, .L134
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L131
	ldr	r3, .L134
	ldr	r3, [r3]
	str	r3, [fp, #-80]
	ldr	r3, [fp, #-80]
	ldr	r3, [r3]
	str	r3, [fp, #-84]
	ldr	r3, [fp, #-84]
	b	.L124
.L131:
	mov	r3, #0
	str	r3, [fp, #-84]
	ldr	r3, [fp, #-84]
	b	.L124
.L130:
	ldr	r3, [fp, #-84]
.L124:
	mov	r0, r3
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
.L135:
	.align	2
.L134:
	.word	head
	.size	__utac__error_stack_mgt, .-__utac__error_stack_mgt
	.section	.rodata
	.align	2
.LC9:
	.ascii	"__utac__get_this_arg\000"
	.align	2
.LC10:
	.ascii	"libacc.c\000"
	.align	2
.LC11:
	.ascii	"i > 0 && i <= this->argsCount\000"
	.text
	.align	2
	.global	__utac__get_this_arg
	.syntax unified
	.arm
	.fpu softvfp
	.type	__utac__get_this_arg, %function
__utac__get_this_arg:
	@ args = 0, pretend = 0, frame = 56
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #56
	str	r0, [fp, #-56]
	str	r1, [fp, #-60]
	ldr	r3, [fp, #-56]
	cmp	r3, #0
	ble	.L137
	ldr	r3, [fp, #-60]
	str	r3, [fp, #-48]
	ldr	r3, [fp, #-48]
	add	r3, r3, #16
	str	r3, [fp, #-44]
	ldr	r3, [fp, #-44]
	str	r3, [fp, #-40]
	ldr	r3, [fp, #-40]
	ldr	r3, [r3]
	str	r3, [fp, #-36]
	ldr	r2, [fp, #-56]
	ldr	r3, [fp, #-36]
	cmp	r2, r3
	ble	.L138
	ldr	r3, .L140
	mov	r2, #123
	ldr	r1, .L140+4
	ldr	r0, .L140+8
	bl	__assert_fail
.L137:
	ldr	r3, .L140
	mov	r2, #123
	ldr	r1, .L140+4
	ldr	r0, .L140+8
	bl	__assert_fail
.L138:
	ldr	r3, [fp, #-56]
	sub	r3, r3, #1
	str	r3, [fp, #-32]
	ldr	r3, [fp, #-60]
	str	r3, [fp, #-28]
	ldr	r3, [fp, #-28]
	add	r3, r3, #8
	str	r3, [fp, #-24]
	ldr	r3, [fp, #-24]
	str	r3, [fp, #-20]
	ldr	r3, [fp, #-20]
	ldr	r3, [r3]
	str	r3, [fp, #-16]
	ldr	r3, [fp, #-32]
	lsl	r3, r3, #2
	ldr	r2, [fp, #-16]
	add	r3, r2, r3
	str	r3, [fp, #-12]
	ldr	r3, [fp, #-12]
	ldr	r3, [r3]
	str	r3, [fp, #-8]
	ldr	r3, [fp, #-8]
	mov	r0, r3
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
.L141:
	.align	2
.L140:
	.word	.LC9
	.word	.LC10
	.word	.LC11
	.size	__utac__get_this_arg, .-__utac__get_this_arg
	.section	.rodata
	.align	2
.LC12:
	.ascii	"__utac__get_this_argtype\000"
	.text
	.align	2
	.global	__utac__get_this_argtype
	.syntax unified
	.arm
	.fpu softvfp
	.type	__utac__get_this_argtype, %function
__utac__get_this_argtype:
	@ args = 0, pretend = 0, frame = 56
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #56
	str	r0, [fp, #-56]
	str	r1, [fp, #-60]
	ldr	r3, [fp, #-56]
	cmp	r3, #0
	ble	.L143
	ldr	r3, [fp, #-60]
	str	r3, [fp, #-48]
	ldr	r3, [fp, #-48]
	add	r3, r3, #16
	str	r3, [fp, #-44]
	ldr	r3, [fp, #-44]
	str	r3, [fp, #-40]
	ldr	r3, [fp, #-40]
	ldr	r3, [r3]
	str	r3, [fp, #-36]
	ldr	r2, [fp, #-56]
	ldr	r3, [fp, #-36]
	cmp	r2, r3
	ble	.L144
	ldr	r3, .L146
	mov	r2, #131
	ldr	r1, .L146+4
	ldr	r0, .L146+8
	bl	__assert_fail
.L143:
	ldr	r3, .L146
	mov	r2, #131
	ldr	r1, .L146+4
	ldr	r0, .L146+8
	bl	__assert_fail
.L144:
	ldr	r3, [fp, #-56]
	sub	r3, r3, #1
	str	r3, [fp, #-32]
	ldr	r3, [fp, #-60]
	str	r3, [fp, #-28]
	ldr	r3, [fp, #-28]
	add	r3, r3, #24
	str	r3, [fp, #-24]
	ldr	r3, [fp, #-24]
	str	r3, [fp, #-20]
	ldr	r3, [fp, #-20]
	ldr	r3, [r3]
	str	r3, [fp, #-16]
	ldr	r3, [fp, #-32]
	lsl	r3, r3, #2
	ldr	r2, [fp, #-16]
	add	r3, r2, r3
	str	r3, [fp, #-12]
	ldr	r3, [fp, #-12]
	ldr	r3, [r3]
	str	r3, [fp, #-8]
	ldr	r3, [fp, #-8]
	mov	r0, r3
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
.L147:
	.align	2
.L146:
	.word	.LC12
	.word	.LC10
	.word	.LC11
	.size	__utac__get_this_argtype, .-__utac__get_this_argtype
	.global	cleanupTimeShifts
	.data
	.align	2
	.type	cleanupTimeShifts, %object
	.size	cleanupTimeShifts, 4
cleanupTimeShifts:
	.word	4
	.text
	.align	2
	.global	cleanup
	.syntax unified
	.arm
	.fpu softvfp
	.type	cleanup, %function
cleanup:
	@ args = 0, pretend = 0, frame = 8
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #8
	bl	timeShift
	mov	r3, #0
	str	r3, [fp, #-12]
.L149:
	ldr	r3, .L155
	ldr	r3, [r3]
	sub	r3, r3, #1
	str	r3, [fp, #-8]
	ldr	r2, [fp, #-12]
	ldr	r3, [fp, #-8]
	cmp	r2, r3
	bge	.L154
	bl	timeShift
	ldr	r3, [fp, #-12]
	add	r3, r3, #1
	str	r3, [fp, #-12]
	b	.L149
.L154:
	nop
.L151:
	nop
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
.L156:
	.align	2
.L155:
	.word	cleanupTimeShifts
	.size	cleanup, .-cleanup
	.align	2
	.global	Specification2
	.syntax unified
	.arm
	.fpu softvfp
	.type	Specification2, %function
Specification2:
	@ args = 0, pretend = 0, frame = 0
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	bl	timeShift
	bl	printPump
	bl	timeShift
	bl	printPump
	bl	timeShift
	bl	printPump
	bl	waterRise
	bl	printPump
	bl	timeShift
	bl	printPump
	bl	changeMethaneLevel
	bl	printPump
	bl	timeShift
	bl	printPump
	bl	cleanup
	nop
	pop	{fp, pc}
	.size	Specification2, .-Specification2
	.align	2
	.global	setup
	.syntax unified
	.arm
	.fpu softvfp
	.type	setup, %function
setup:
	@ 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	setup, .-setup
	.align	2
	.global	runTest
	.syntax unified
	.arm
	.fpu softvfp
	.type	runTest, %function
runTest:
	@ args = 0, pretend = 0, frame = 0
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	bl	test
	nop
	pop	{fp, pc}
	.size	runTest, .-runTest
	.align	2
	.global	main
	.syntax unified
	.arm
	.fpu softvfp
	.type	main, %function
main:
	@ args = 0, pretend = 0, frame = 8
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	sub	sp, sp, #8
	bl	select_helpers
	bl	select_features
	bl	valid_product
	str	r0, [fp, #-12]
	ldr	r3, [fp, #-12]
	cmp	r3, #0
	beq	.L164
	bl	setup
	bl	runTest
.L164:
	mov	r3, #0
	str	r3, [fp, #-8]
	ldr	r3, [fp, #-8]
	mov	r0, r3
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
	.size	main, .-main
	.ident	"GCC: (Ubuntu 9.4.0-1ubuntu1~20.04.2) 9.4.0"
	.section	.note.GNU-stack,"",%progbits
