	.file	"225141897.c"
	.intel_syntax noprefix
	.text
	.globl	methAndRunningLastTime
	.bss
	.align 4
	.type	methAndRunningLastTime, @object
	.size	methAndRunningLastTime, 4
methAndRunningLastTime:
	.zero	4
	.text
	.type	__utac_acc__Specification2_spec__1, @function
__utac_acc__Specification2_spec__1:
.LFB0:
	.cfi_startproc
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	mov	DWORD PTR methAndRunningLastTime[rip], 0
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE0:
	.size	__utac_acc__Specification2_spec__1, .-__utac_acc__Specification2_spec__1
	.type	__utac_acc__Specification2_spec__2, @function
__utac_acc__Specification2_spec__2:
.LFB1:
	.cfi_startproc
	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 -8[rbp], eax
	cmp	DWORD PTR -8[rbp], 0
	je	.L4
	call	isPumpRunning
	mov	DWORD PTR -4[rbp], eax
	cmp	DWORD PTR -4[rbp], 0
	je	.L5
	mov	eax, DWORD PTR methAndRunningLastTime[rip]
	test	eax, eax
	je	.L6
	call	__automaton_fail
	jmp	.L3
.L6:
	mov	DWORD PTR methAndRunningLastTime[rip], 1
	jmp	.L3
.L5:
	mov	DWORD PTR methAndRunningLastTime[rip], 0
	jmp	.L3
.L4:
	mov	DWORD PTR methAndRunningLastTime[rip], 0
	nop
.L3:
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE1:
	.size	__utac_acc__Specification2_spec__2, .-__utac_acc__Specification2_spec__2
	.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:
.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 waterLevel[rip]
	test	eax, eax
	jle	.L12
	mov	eax, DWORD PTR waterLevel[rip]
	sub	eax, 1
	mov	DWORD PTR waterLevel[rip], eax
	nop
.L12:
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE2:
	.size	lowerWaterLevel, .-lowerWaterLevel
	.globl	waterRise
	.type	waterRise, @function
waterRise:
.LFB3:
	.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	.L16
	mov	eax, DWORD PTR waterLevel[rip]
	add	eax, 1
	mov	DWORD PTR waterLevel[rip], eax
	nop
.L16:
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE3:
	.size	waterRise, .-waterRise
	.globl	changeMethaneLevel
	.type	changeMethaneLevel, @function
changeMethaneLevel:
.LFB4:
	.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	.L18
	mov	DWORD PTR methaneLevelCritical[rip], 0
	jmp	.L17
.L18:
	mov	DWORD PTR methaneLevelCritical[rip], 1
	nop
.L17:
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE4:
	.size	changeMethaneLevel, .-changeMethaneLevel
	.globl	isMethaneLevelCritical
	.type	isMethaneLevelCritical, @function
isMethaneLevelCritical:
.LFB5:
	.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
.LFE5:
	.size	isMethaneLevelCritical, .-isMethaneLevelCritical
	.section	.rodata
.LC0:
	.string	"Env(Water:%i"
.LC1:
	.string	",Meth:"
.LC2:
	.string	"CRIT"
.LC3:
	.string	"OK"
	.text
	.globl	printEnvironment
	.type	printEnvironment, @function
printEnvironment:
.LFB6:
	.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, .LC0[rip]
	mov	eax, 0
	call	printf@PLT
	lea	rdi, .LC1[rip]
	mov	eax, 0
	call	printf@PLT
	mov	eax, DWORD PTR methaneLevelCritical[rip]
	test	eax, eax
	je	.L24
	lea	rdi, .LC2[rip]
	mov	eax, 0
	call	printf@PLT
	jmp	.L25
.L24:
	lea	rdi, .LC3[rip]
	mov	eax, 0
	call	printf@PLT
.L25:
	mov	edi, 41
	call	putchar@PLT
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE6:
	.size	printEnvironment, .-printEnvironment
	.globl	getWaterLevel
	.type	getWaterLevel, @function
getWaterLevel:
.LFB7:
	.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
.LFE7:
	.size	getWaterLevel, .-getWaterLevel
	.globl	isHighWaterSensorDry
	.type	isHighWaterSensorDry, @function
isHighWaterSensorDry:
.LFB8:
	.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	.L30
	mov	DWORD PTR -4[rbp], 1
	mov	eax, DWORD PTR -4[rbp]
	jmp	.L31
.L30:
	mov	DWORD PTR -4[rbp], 0
	mov	eax, DWORD PTR -4[rbp]
.L31:
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE8:
	.size	isHighWaterSensorDry, .-isHighWaterSensorDry
	.globl	test
	.type	test, @function
test:
.LFB9:
	.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
.L33:
	cmp	DWORD PTR -20[rbp], 3
	jg	.L42
	call	__VERIFIER_nondet_int@PLT
	mov	DWORD PTR -16[rbp], eax
	cmp	DWORD PTR -16[rbp], 0
	je	.L36
	call	waterRise
.L36:
	call	__VERIFIER_nondet_int@PLT
	mov	DWORD PTR -12[rbp], eax
	cmp	DWORD PTR -12[rbp], 0
	je	.L37
	call	changeMethaneLevel
.L37:
	call	__VERIFIER_nondet_int@PLT
	mov	DWORD PTR -8[rbp], eax
	cmp	DWORD PTR -8[rbp], 0
	je	.L38
	call	startSystem
	jmp	.L39
.L38:
	call	__VERIFIER_nondet_int@PLT
	mov	DWORD PTR -4[rbp], eax
	cmp	DWORD PTR -4[rbp], 0
	je	.L39
	call	stopSystem
.L39:
	call	timeShift
	jmp	.L33
.L42:
	nop
.L35:
	call	cleanup
	nop
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE9:
	.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:
.LFB10:
	.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	.L44
	call	lowerWaterLevel
.L44:
	mov	eax, DWORD PTR systemActive[rip]
	test	eax, eax
	je	.L45
	call	processEnvironment
.L45:
	call	__utac_acc__Specification2_spec__2
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE10:
	.size	timeShift, .-timeShift
	.globl	processEnvironment__wrappee__base
	.type	processEnvironment__wrappee__base, @function
processEnvironment__wrappee__base:
.LFB11:
	.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
.LFE11:
	.size	processEnvironment__wrappee__base, .-processEnvironment__wrappee__base
	.globl	processEnvironment__wrappee__highWaterSensor
	.type	processEnvironment__wrappee__highWaterSensor, @function
processEnvironment__wrappee__highWaterSensor:
.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
	mov	eax, DWORD PTR pumpRunning[rip]
	test	eax, eax
	jne	.L50
	call	isHighWaterLevel
	mov	DWORD PTR -4[rbp], eax
	cmp	DWORD PTR -4[rbp], 0
	je	.L51
	call	activatePump
	jmp	.L49
.L51:
	call	processEnvironment__wrappee__base
	jmp	.L49
.L50:
	call	processEnvironment__wrappee__base
	nop
.L49:
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE12:
	.size	processEnvironment__wrappee__highWaterSensor, .-processEnvironment__wrappee__highWaterSensor
	.globl	processEnvironment
	.type	processEnvironment, @function
processEnvironment:
.LFB13:
	.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	.L55
	call	isMethaneAlarm
	mov	DWORD PTR -4[rbp], eax
	cmp	DWORD PTR -4[rbp], 0
	je	.L56
	call	deactivatePump
	jmp	.L54
.L56:
	call	processEnvironment__wrappee__highWaterSensor
	jmp	.L54
.L55:
	call	processEnvironment__wrappee__highWaterSensor
	nop
.L54:
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE13:
	.size	processEnvironment, .-processEnvironment
	.globl	activatePump
	.type	activatePump, @function
activatePump:
.LFB14:
	.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
.LFE14:
	.size	activatePump, .-activatePump
	.globl	deactivatePump
	.type	deactivatePump, @function
deactivatePump:
.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 pumpRunning[rip], 0
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE15:
	.size	deactivatePump, .-deactivatePump
	.globl	isMethaneAlarm
	.type	isMethaneAlarm, @function
isMethaneAlarm:
.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	isMethaneLevelCritical
	mov	DWORD PTR -4[rbp], eax
	mov	eax, DWORD PTR -4[rbp]
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE16:
	.size	isMethaneAlarm, .-isMethaneAlarm
	.globl	isPumpRunning
	.type	isPumpRunning, @function
isPumpRunning:
.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 pumpRunning[rip]
	mov	DWORD PTR -4[rbp], eax
	mov	eax, DWORD PTR -4[rbp]
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE17:
	.size	isPumpRunning, .-isPumpRunning
	.section	.rodata
.LC4:
	.string	"Pump(System:"
.LC5:
	.string	"On"
.LC6:
	.string	"Off"
.LC7:
	.string	",Pump:"
.LC8:
	.string	") "
	.text
	.globl	printPump
	.type	printPump, @function
printPump:
.LFB18:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	lea	rdi, .LC4[rip]
	mov	eax, 0
	call	printf@PLT
	mov	eax, DWORD PTR systemActive[rip]
	test	eax, eax
	je	.L68
	lea	rdi, .LC5[rip]
	mov	eax, 0
	call	printf@PLT
	jmp	.L69
.L68:
	lea	rdi, .LC6[rip]
	mov	eax, 0
	call	printf@PLT
.L69:
	lea	rdi, .LC7[rip]
	mov	eax, 0
	call	printf@PLT
	mov	eax, DWORD PTR pumpRunning[rip]
	test	eax, eax
	je	.L70
	lea	rdi, .LC5[rip]
	mov	eax, 0
	call	printf@PLT
	jmp	.L71
.L70:
	lea	rdi, .LC6[rip]
	mov	eax, 0
	call	printf@PLT
.L71:
	lea	rdi, .LC8[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
.LFE18:
	.size	printPump, .-printPump
	.globl	isHighWaterLevel
	.type	isHighWaterLevel, @function
isHighWaterLevel:
.LFB19:
	.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	isHighWaterSensorDry
	mov	DWORD PTR -8[rbp], eax
	cmp	DWORD PTR -8[rbp], 0
	je	.L74
	mov	DWORD PTR -12[rbp], 0
	jmp	.L75
.L74:
	mov	DWORD PTR -12[rbp], 1
.L75:
	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
.LFE19:
	.size	isHighWaterLevel, .-isHighWaterLevel
	.globl	stopSystem
	.type	stopSystem, @function
stopSystem:
.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 pumpRunning[rip]
	test	eax, eax
	je	.L78
	call	deactivatePump
.L78:
	mov	DWORD PTR systemActive[rip], 0
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE20:
	.size	stopSystem, .-stopSystem
	.globl	startSystem
	.type	startSystem, @function
startSystem:
.LFB21:
	.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 systemActive[rip], 1
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE21:
	.size	startSystem, .-startSystem
	.globl	__utac__exception__cf_handler_set
	.type	__utac__exception__cf_handler_set, @function
__utac__exception__cf_handler_set:
.LFB22:
	.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
.LFE22:
	.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:
.LFB23:
	.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
.L85:
	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	.L90
	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	.L85
.L90:
	nop
.L87:
	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
.LFE23:
	.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:
.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 -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
.L92:
	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	.L97
	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	.L92
.L97:
	nop
.L94:
	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
.LFE24:
	.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:
.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, 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	.L99
	mov	rax, QWORD PTR -160[rbp]
	jmp	.L100
.L99:
	cmp	DWORD PTR -188[rbp], 0
	jne	.L101
	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	.L100
.L101:
	cmp	DWORD PTR -188[rbp], 1
	jne	.L102
	mov	rax, QWORD PTR head[rip]
	mov	QWORD PTR -168[rbp], rax
.L103:
	cmp	DWORD PTR -192[rbp], 1
	jle	.L109
	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	.L103
.L109:
	nop
.L105:
	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	.L100
.L102:
	cmp	DWORD PTR -188[rbp], 2
	jne	.L106
	mov	rax, QWORD PTR head[rip]
	test	rax, rax
	je	.L107
	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	.L100
.L107:
	mov	QWORD PTR -160[rbp], 0
	mov	rax, QWORD PTR -160[rbp]
	jmp	.L100
.L106:
	mov	rax, QWORD PTR -160[rbp]
.L100:
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE25:
	.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:
.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, 96
	mov	DWORD PTR -84[rbp], edi
	mov	QWORD PTR -96[rbp], rsi
	cmp	DWORD PTR -84[rbp], 0
	jle	.L111
	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	.L112
	lea	rcx, .LC9[rip]
	mov	edx, 123
	lea	rsi, .LC10[rip]
	lea	rdi, .LC11[rip]
	call	__assert_fail@PLT
.L111:
	lea	rcx, .LC9[rip]
	mov	edx, 123
	lea	rsi, .LC10[rip]
	lea	rdi, .LC11[rip]
	call	__assert_fail@PLT
.L112:
	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
.LFE26:
	.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:
.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, 96
	mov	DWORD PTR -84[rbp], edi
	mov	QWORD PTR -96[rbp], rsi
	cmp	DWORD PTR -84[rbp], 0
	jle	.L115
	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	.L116
	lea	rcx, .LC12[rip]
	mov	edx, 131
	lea	rsi, .LC10[rip]
	lea	rdi, .LC11[rip]
	call	__assert_fail@PLT
.L115:
	lea	rcx, .LC12[rip]
	mov	edx, 131
	lea	rsi, .LC10[rip]
	lea	rdi, .LC11[rip]
	call	__assert_fail@PLT
.L116:
	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
.LFE27:
	.size	__utac__get_this_argtype, .-__utac__get_this_argtype
	.globl	__automaton_fail
	.type	__automaton_fail, @function
__automaton_fail:
.LFB28:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
.L119:
	mov	eax, 0
	call	__VERIFIER_error@PLT
	.cfi_endproc
.LFE28:
	.size	__automaton_fail, .-__automaton_fail
	.globl	cleanupTimeShifts
	.data
	.align 4
	.type	cleanupTimeShifts, @object
	.size	cleanupTimeShifts, 4
cleanupTimeShifts:
	.long	4
	.text
	.globl	cleanup
	.type	cleanup, @function
cleanup:
.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, 16
	call	timeShift
	mov	DWORD PTR -8[rbp], 0
.L121:
	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	.L126
	call	timeShift
	add	DWORD PTR -8[rbp], 1
	jmp	.L121
.L126:
	nop
.L123:
	nop
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE29:
	.size	cleanup, .-cleanup
	.globl	Specification2
	.type	Specification2, @function
Specification2:
.LFB30:
	.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
.LFE30:
	.size	Specification2, .-Specification2
	.globl	setup
	.type	setup, @function
setup:
.LFB31:
	.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
.LFE31:
	.size	setup, .-setup
	.globl	runTest
	.type	runTest, @function
runTest:
.LFB32:
	.cfi_startproc
	endbr64
	push	rbp
	.cfi_def_cfa_offset 16
	.cfi_offset 6, -16
	mov	rbp, rsp
	.cfi_def_cfa_register 6
	call	__utac_acc__Specification2_spec__1
	call	test
	nop
	pop	rbp
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE32:
	.size	runTest, .-runTest
	.globl	main
	.type	main, @function
main:
.LFB33:
	.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	.L134
	call	setup
	call	runTest
.L134:
	mov	DWORD PTR -4[rbp], 0
	mov	eax, DWORD PTR -4[rbp]
	leave
	.cfi_def_cfa 7, 8
	ret
	.cfi_endproc
.LFE33:
	.size	main, .-main
	.globl	select_one
	.type	select_one, @function
select_one:
.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	__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
.LFE34:
	.size	select_one, .-select_one
	.globl	select_features
	.type	select_features, @function
select_features:
.LFB35:
	.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
.LFE35:
	.size	select_features, .-select_features
	.globl	select_helpers
	.type	select_helpers, @function
select_helpers:
.LFB36:
	.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
.LFE36:
	.size	select_helpers, .-select_helpers
	.globl	valid_product
	.type	valid_product, @function
valid_product:
.LFB37:
	.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
.LFE37:
	.size	valid_product, .-valid_product
	.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	"225141897.c"
	.text
	.comm	methAndRunningLastTime,4,4
	.align	2
	.syntax unified
	.arm
	.fpu softvfp
	.type	__utac_acc__Specification2_spec__1, %function
__utac_acc__Specification2_spec__1:
	@ 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, .L3
	mov	r2, #0
	str	r2, [r3]
	nop
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
.L4:
	.align	2
.L3:
	.word	methAndRunningLastTime
	.size	__utac_acc__Specification2_spec__1, .-__utac_acc__Specification2_spec__1
	.align	2
	.syntax unified
	.arm
	.fpu softvfp
	.type	__utac_acc__Specification2_spec__2, %function
__utac_acc__Specification2_spec__2:
	@ 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, #-12]
	ldr	r3, [fp, #-12]
	cmp	r3, #0
	beq	.L6
	bl	isPumpRunning
	str	r0, [fp, #-8]
	ldr	r3, [fp, #-8]
	cmp	r3, #0
	beq	.L7
	ldr	r3, .L11
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L8
	bl	__automaton_fail
	b	.L5
.L8:
	ldr	r3, .L11
	mov	r2, #1
	str	r2, [r3]
	b	.L5
.L7:
	ldr	r3, .L11
	mov	r2, #0
	str	r2, [r3]
	b	.L5
.L6:
	ldr	r3, .L11
	mov	r2, #0
	str	r2, [r3]
	nop
.L5:
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
.L12:
	.align	2
.L11:
	.word	methAndRunningLastTime
	.size	__utac_acc__Specification2_spec__2, .-__utac_acc__Specification2_spec__2
	.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, .L17
	ldr	r3, [r3]
	cmp	r3, #0
	ble	.L16
	ldr	r3, .L17
	ldr	r3, [r3]
	sub	r3, r3, #1
	ldr	r2, .L17
	str	r3, [r2]
	nop
.L16:
	nop
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
.L18:
	.align	2
.L17:
	.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, .L23
	ldr	r3, [r3]
	cmp	r3, #1
	bgt	.L22
	ldr	r3, .L23
	ldr	r3, [r3]
	add	r3, r3, #1
	ldr	r2, .L23
	str	r3, [r2]
	nop
.L22:
	nop
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
.L24:
	.align	2
.L23:
	.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, .L29
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L26
	ldr	r3, .L29
	mov	r2, #0
	str	r2, [r3]
	b	.L25
.L26:
	ldr	r3, .L29
	mov	r2, #1
	str	r2, [r3]
	nop
.L25:
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
.L30:
	.align	2
.L29:
	.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, .L33
	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
.L34:
	.align	2
.L33:
	.word	methaneLevelCritical
	.size	isMethaneLevelCritical, .-isMethaneLevelCritical
	.section	.rodata
	.align	2
.LC0:
	.ascii	"Env(Water:%i\000"
	.align	2
.LC1:
	.ascii	",Meth:\000"
	.align	2
.LC2:
	.ascii	"CRIT\000"
	.align	2
.LC3:
	.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, .L39
	ldr	r3, [r3]
	mov	r1, r3
	ldr	r0, .L39+4
	bl	printf
	ldr	r0, .L39+8
	bl	printf
	ldr	r3, .L39+12
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L36
	ldr	r0, .L39+16
	bl	printf
	b	.L37
.L36:
	ldr	r0, .L39+20
	bl	printf
.L37:
	mov	r0, #41
	bl	putchar
	nop
	pop	{fp, pc}
.L40:
	.align	2
.L39:
	.word	waterLevel
	.word	.LC0
	.word	.LC1
	.word	methaneLevelCritical
	.word	.LC2
	.word	.LC3
	.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, .L43
	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
.L44:
	.align	2
.L43:
	.word	waterLevel
	.size	getWaterLevel, .-getWaterLevel
	.align	2
	.global	isHighWaterSensorDry
	.syntax unified
	.arm
	.fpu softvfp
	.type	isHighWaterSensorDry, %function
isHighWaterSensorDry:
	@ 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, .L48
	ldr	r3, [r3]
	cmp	r3, #1
	bgt	.L46
	mov	r3, #1
	str	r3, [fp, #-8]
	ldr	r3, [fp, #-8]
	b	.L47
.L46:
	mov	r3, #0
	str	r3, [fp, #-8]
	ldr	r3, [fp, #-8]
.L47:
	mov	r0, r3
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
.L49:
	.align	2
.L48:
	.word	waterLevel
	.size	isHighWaterSensorDry, .-isHighWaterSensorDry
	.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]
.L51:
	ldr	r3, [fp, #-24]
	cmp	r3, #3
	bgt	.L60
	bl	__VERIFIER_nondet_int
	str	r0, [fp, #-20]
	ldr	r3, [fp, #-20]
	cmp	r3, #0
	beq	.L54
	bl	waterRise
.L54:
	bl	__VERIFIER_nondet_int
	str	r0, [fp, #-16]
	ldr	r3, [fp, #-16]
	cmp	r3, #0
	beq	.L55
	bl	changeMethaneLevel
.L55:
	bl	__VERIFIER_nondet_int
	str	r0, [fp, #-12]
	ldr	r3, [fp, #-12]
	cmp	r3, #0
	beq	.L56
	bl	startSystem
	b	.L57
.L56:
	bl	__VERIFIER_nondet_int
	str	r0, [fp, #-8]
	ldr	r3, [fp, #-8]
	cmp	r3, #0
	beq	.L57
	bl	stopSystem
.L57:
	bl	timeShift
	b	.L51
.L60:
	nop
.L53:
	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, .L65
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L62
	bl	lowerWaterLevel
.L62:
	ldr	r3, .L65+4
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L63
	bl	processEnvironment
.L63:
	bl	__utac_acc__Specification2_spec__2
	nop
	pop	{fp, pc}
.L66:
	.align	2
.L65:
	.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__wrappee__highWaterSensor
	.syntax unified
	.arm
	.fpu softvfp
	.type	processEnvironment__wrappee__highWaterSensor, %function
processEnvironment__wrappee__highWaterSensor:
	@ 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, .L74
	ldr	r3, [r3]
	cmp	r3, #0
	bne	.L70
	bl	isHighWaterLevel
	str	r0, [fp, #-8]
	ldr	r3, [fp, #-8]
	cmp	r3, #0
	beq	.L71
	bl	activatePump
	b	.L69
.L71:
	bl	processEnvironment__wrappee__base
	b	.L69
.L70:
	bl	processEnvironment__wrappee__base
	nop
.L69:
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
.L75:
	.align	2
.L74:
	.word	pumpRunning
	.size	processEnvironment__wrappee__highWaterSensor, .-processEnvironment__wrappee__highWaterSensor
	.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, .L81
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L77
	bl	isMethaneAlarm
	str	r0, [fp, #-8]
	ldr	r3, [fp, #-8]
	cmp	r3, #0
	beq	.L78
	bl	deactivatePump
	b	.L76
.L78:
	bl	processEnvironment__wrappee__highWaterSensor
	b	.L76
.L77:
	bl	processEnvironment__wrappee__highWaterSensor
	nop
.L76:
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
.L82:
	.align	2
.L81:
	.word	pumpRunning
	.size	processEnvironment, .-processEnvironment
	.align	2
	.global	activatePump
	.syntax unified
	.arm
	.fpu softvfp
	.type	activatePump, %function
activatePump:
	@ 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, .L85
	mov	r2, #1
	str	r2, [r3]
	nop
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
.L86:
	.align	2
.L85:
	.word	pumpRunning
	.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, .L89
	mov	r2, #0
	str	r2, [r3]
	nop
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
.L90:
	.align	2
.L89:
	.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, .L95
	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
.L96:
	.align	2
.L95:
	.word	pumpRunning
	.size	isPumpRunning, .-isPumpRunning
	.section	.rodata
	.align	2
.LC4:
	.ascii	"Pump(System:\000"
	.align	2
.LC5:
	.ascii	"On\000"
	.align	2
.LC6:
	.ascii	"Off\000"
	.align	2
.LC7:
	.ascii	",Pump:\000"
	.align	2
.LC8:
	.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, .L103
	bl	printf
	ldr	r3, .L103+4
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L98
	ldr	r0, .L103+8
	bl	printf
	b	.L99
.L98:
	ldr	r0, .L103+12
	bl	printf
.L99:
	ldr	r0, .L103+16
	bl	printf
	ldr	r3, .L103+20
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L100
	ldr	r0, .L103+8
	bl	printf
	b	.L101
.L100:
	ldr	r0, .L103+12
	bl	printf
.L101:
	ldr	r0, .L103+24
	bl	printf
	bl	printEnvironment
	mov	r0, #10
	bl	putchar
	nop
	pop	{fp, pc}
.L104:
	.align	2
.L103:
	.word	.LC4
	.word	systemActive
	.word	.LC5
	.word	.LC6
	.word	.LC7
	.word	pumpRunning
	.word	.LC8
	.size	printPump, .-printPump
	.align	2
	.global	isHighWaterLevel
	.syntax unified
	.arm
	.fpu softvfp
	.type	isHighWaterLevel, %function
isHighWaterLevel:
	@ 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	isHighWaterSensorDry
	str	r0, [fp, #-12]
	ldr	r3, [fp, #-12]
	cmp	r3, #0
	beq	.L106
	mov	r3, #0
	str	r3, [fp, #-16]
	b	.L107
.L106:
	mov	r3, #1
	str	r3, [fp, #-16]
.L107:
	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	isHighWaterLevel, .-isHighWaterLevel
	.align	2
	.global	stopSystem
	.syntax unified
	.arm
	.fpu softvfp
	.type	stopSystem, %function
stopSystem:
	@ args = 0, pretend = 0, frame = 0
	@ frame_needed = 1, uses_anonymous_args = 0
	push	{fp, lr}
	add	fp, sp, #4
	ldr	r3, .L112
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L110
	bl	deactivatePump
.L110:
	ldr	r3, .L112+4
	mov	r2, #0
	str	r2, [r3]
	nop
	pop	{fp, pc}
.L113:
	.align	2
.L112:
	.word	pumpRunning
	.word	systemActive
	.size	stopSystem, .-stopSystem
	.align	2
	.global	startSystem
	.syntax unified
	.arm
	.fpu softvfp
	.type	startSystem, %function
startSystem:
	@ 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, .L116
	mov	r2, #1
	str	r2, [r3]
	nop
	add	sp, fp, #0
	@ sp needed
	ldr	fp, [sp], #4
	bx	lr
.L117:
	.align	2
.L116:
	.word	systemActive
	.size	startSystem, .-startSystem
	.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]
.L121:
	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	.L126
	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	.L121
.L126:
	nop
.L123:
	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]
.L128:
	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	.L133
	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	.L128
.L133:
	nop
.L130:
	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	.L135
	ldr	r3, [fp, #-84]
	b	.L136
.L135:
	ldr	r3, [fp, #-100]
	cmp	r3, #0
	bne	.L137
	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, .L146
	ldr	r2, [r3]
	ldr	r3, [fp, #-8]
	str	r2, [r3]
	ldr	r2, .L146
	ldr	r3, [fp, #-24]
	str	r3, [r2]
	ldr	r3, [fp, #-24]
	str	r3, [fp, #-84]
	ldr	r3, [fp, #-84]
	b	.L136
.L137:
	ldr	r3, [fp, #-100]
	cmp	r3, #1
	bne	.L138
	ldr	r3, .L146
	ldr	r3, [r3]
	str	r3, [fp, #-88]
.L139:
	ldr	r3, [fp, #-104]
	cmp	r3, #1
	ble	.L145
	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	.L139
.L145:
	nop
.L141:
	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, .L146
	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	.L136
.L138:
	ldr	r3, [fp, #-100]
	cmp	r3, #2
	bne	.L142
	ldr	r3, .L146
	ldr	r3, [r3]
	cmp	r3, #0
	beq	.L143
	ldr	r3, .L146
	ldr	r3, [r3]
	str	r3, [fp, #-80]
	ldr	r3, [fp, #-80]
	ldr	r3, [r3]
	str	r3, [fp, #-84]
	ldr	r3, [fp, #-84]
	b	.L136
.L143:
	mov	r3, #0
	str	r3, [fp, #-84]
	ldr	r3, [fp, #-84]
	b	.L136
.L142:
	ldr	r3, [fp, #-84]
.L136:
	mov	r0, r3
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
.L147:
	.align	2
.L146:
	.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	.L149
	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	.L150
	ldr	r3, .L152
	mov	r2, #123
	ldr	r1, .L152+4
	ldr	r0, .L152+8
	bl	__assert_fail
.L149:
	ldr	r3, .L152
	mov	r2, #123
	ldr	r1, .L152+4
	ldr	r0, .L152+8
	bl	__assert_fail
.L150:
	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}
.L153:
	.align	2
.L152:
	.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	.L155
	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	.L156
	ldr	r3, .L158
	mov	r2, #131
	ldr	r1, .L158+4
	ldr	r0, .L158+8
	bl	__assert_fail
.L155:
	ldr	r3, .L158
	mov	r2, #131
	ldr	r1, .L158+4
	ldr	r0, .L158+8
	bl	__assert_fail
.L156:
	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}
.L159:
	.align	2
.L158:
	.word	.LC12
	.word	.LC10
	.word	.LC11
	.size	__utac__get_this_argtype, .-__utac__get_this_argtype
	.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
.L161:
	bl	__VERIFIER_error
	.size	__automaton_fail, .-__automaton_fail
	.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]
.L163:
	ldr	r3, .L169
	ldr	r3, [r3]
	sub	r3, r3, #1
	str	r3, [fp, #-8]
	ldr	r2, [fp, #-12]
	ldr	r3, [fp, #-8]
	cmp	r2, r3
	bge	.L168
	bl	timeShift
	ldr	r3, [fp, #-12]
	add	r3, r3, #1
	str	r3, [fp, #-12]
	b	.L163
.L168:
	nop
.L165:
	nop
	sub	sp, fp, #4
	@ sp needed
	pop	{fp, pc}
.L170:
	.align	2
.L169:
	.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	__utac_acc__Specification2_spec__1
	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	.L178
	bl	setup
	bl	runTest
.L178:
	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
	.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
	.ident	"GCC: (Ubuntu 9.4.0-1ubuntu1~20.04.2) 9.4.0"
	.section	.note.GNU-stack,"",%progbits
