cs_time_var_mutex_true-unreach-call.i_0.smt2 34.8 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
(set-info :smt-lib-version 2.6)
(set-logic QF_ALIA)
(set-info :source "|
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.

This SMT script belongs to a set of SMT scripts that was generated by
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2019 [5,6].
This script might _not_ contain all SMT commands that are used by
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.

2019-04-27, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)

[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus,
     Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian
     Schilling, Tanja Schindler, Andreas Podelski: Ultimate Automizer
     and the Search for Perfect Interpolants - (Competition Contribution).
     TACAS (2) 2018: 447-451
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model
     Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Automatic Verification of C and Java Programs: SV-COMP 2019.
     TACAS (3) 2019: 133-155
[6] https://sv-comp.sosy-lab.org/2019/
|")
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun |#funAddr~allocator.base| () Int)
(declare-fun |#funAddr~allocator.offset| () Int)
(declare-fun |#funAddr~de_allocator.base| () Int)
(declare-fun |#funAddr~de_allocator.offset| () Int)
(declare-fun |#funAddr~main_thread.base| () Int)
(declare-fun |#funAddr~main_thread.offset| () Int)
(declare-fun ~unnamed0~0~P_ALL () Int)
(declare-fun ~unnamed0~0~P_PID () Int)
(declare-fun ~unnamed0~0~P_PGID () Int)
(assert (and (= 0 |#funAddr~allocator.offset|) (= |#funAddr~allocator.base| (- 1))))
(assert (and (= (- 1) |#funAddr~de_allocator.base|) (= 1 |#funAddr~de_allocator.offset|)))
(assert (and (= 2 |#funAddr~main_thread.offset|) (= |#funAddr~main_thread.base| (- 1))))
(assert (= ~unnamed0~0~P_ALL 0))
(assert (= ~unnamed0~0~P_PID 1))
(assert (= 2 ~unnamed0~0~P_PGID))
(declare-fun |v_#memory_int_69_const_1545201522| () (Array Int (Array Int Int)))
(declare-fun |v_main_~#__CS_cp_block~0.base_6_const_304370259| () Int)
(declare-fun |v_main_~#__CS_cp_block~0.offset_6_const_1469162001| () Int)
(declare-fun |v_~#block~0.base_7_const_-1770608023| () Int)
(declare-fun |v_~#block~0.offset_7_const_283662439| () Int)
(declare-fun |v_main_~#__CS_cp_busy~0.base_6_const_728408393| () Int)
(declare-fun |v_main_~#__CS_cp_busy~0.offset_6_const_956269447| () Int)
(declare-fun |v_~#busy~0.base_6_const_-862540142| () Int)
(declare-fun |v_~#busy~0.offset_6_const_1056451216| () Int)
(declare-fun |v_main_~#__CS_cp_inode~0.base_6_const_-144247247| () Int)
(declare-fun |v_main_~#__CS_cp_inode~0.offset_6_const_-157493745| () Int)
(declare-fun |v_~#inode~0.base_6_const_2075872712| () Int)
(declare-fun |v_~#inode~0.offset_6_const_-1342747578| () Int)
(declare-fun |v_main_~#__CS_cp_m_inode~0.base_6_const_716180767| () Int)
(declare-fun |v_main_~#__CS_cp_m_inode~0.offset_6_const_2084641245| () Int)
(declare-fun |v_~#m_inode~0.base_7_const_-469204139| () Int)
(declare-fun |v_~#m_inode~0.offset_7_const_1100766803| () Int)
(declare-fun |v_main_~#__CS_cp_m_busy~0.base_6_const_617622715| () Int)
(declare-fun |v_main_~#__CS_cp_m_busy~0.offset_6_const_1859883641| () Int)
(declare-fun |v_~#m_busy~0.base_9_const_717935425| () Int)
(declare-fun |v_~#m_busy~0.offset_9_const_-527293729| () Int)
(declare-fun |v_~#__CS_thread_born_round~0.base_3_const_1720302586| () Int)
(declare-fun |v_~#__CS_thread_born_round~0.offset_3_const_544850616| () Int)
(declare-fun v_~__CS_round~0_91_const_-563051970 () Int)
(declare-fun |v_~#__CS_thread_status~0.base_4_const_-48473261| () Int)
(declare-fun |v_~#__CS_thread_status~0.offset_4_const_1684530065| () Int)
(declare-fun v_~__THREAD_RUNNING~0_2_const_278392747 () Int)
(declare-fun |v_~#__CS_thread_allocated~0.base_3_const_1055191041| () Int)
(declare-fun |v_~#__CS_thread_allocated~0.offset_3_const_1454422303| () Int)
(declare-fun |v_#memory_int_56_const_1545201488| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_72_const_1545201418| () (Array Int (Array Int Int)))
(declare-fun |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| () Int)
(declare-fun |v_~#__CS_thread_lockedon~0.offset_5_const_541011271| () Int)
(declare-fun |v_#memory_int_73_const_1545201429| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_55_const_-436731520| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_56_const_-436731517| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_57_const_-475207604| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_58_const_-475207601| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_72_const_-475207673| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_73_const_-475207674| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_59_const_-436731508| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_60_const_-436731494| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_75_const_-436731578| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_76_const_-436731583| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_73_const_-436731580| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_74_const_-436731577| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_71_const_-475207676| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_59_const_-475207602| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_52_const_-475207615| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_53_const_-475207616| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_71_const_-436731462| () (Array Int (Array Int Int)))
(declare-fun |v_main_~#__CS_cp___CS_thread_lockedon~0.base_6_const_-1933732865| () Int)
(declare-fun |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_6_const_-1991001923| () Int)
(declare-fun |v_#memory_$Pointer$.offset_64_const_-436731482| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_74_const_1545201428| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_54_const_-436731519| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_64_const_-475207584| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_61_const_-436731483| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_74_const_-475207679| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_62_const_-475207578| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_63_const_-475207583| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_53_const_-436731514| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_71_const_1545201419| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_55_const_-475207614| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_56_const_-475207603| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_52_const_-436731513| () (Array Int (Array Int Int)))
(declare-fun |v_main_#t~mem77_1_const_204397592| () Int)
(declare-fun |v_#memory_$Pointer$.base_54_const_-475207613| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_60_const_-475207580| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_75_const_-475207680| () (Array Int (Array Int Int)))
(declare-fun v_~__CS_thread~0.base_11_const_-335877311 () (Array Int Int))
(declare-fun v_~__CS_thread~0.base_12_const_-335877312 () (Array Int Int))
(declare-fun v_~__CS_thread_index~0_8_const_-147234547 () Int)
(declare-fun |v_#memory_$Pointer$.base_61_const_-475207577| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_72_const_-436731579| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_62_const_-436731484| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_63_const_-436731481| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_70_const_1545201416| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_77_const_-436731584| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_57_const_-436731518| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_58_const_-436731507| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_76_const_-475207677| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_77_const_-475207678| () (Array Int (Array Int Int)))
(declare-fun v_~__CS_thread~0.offset_11_const_1266608195 () (Array Int Int))
(declare-fun v_~__CS_thread~0.offset_12_const_1266608194 () (Array Int Int))
(declare-fun |v_#memory_int_81_const_1545201448| () (Array Int (Array Int Int)))
(declare-fun |v_main_~#__CS_cp___CS_thread_status~0.base_6_const_1635486152| () Int)
(declare-fun |v_main_~#__CS_cp___CS_thread_status~0.offset_6_const_649365574| () Int)
(assert (let ((.cse9 (select |v_#memory_$Pointer$.base_72_const_-475207673| |v_~#__CS_thread_status~0.base_4_const_-48473261|)) (.cse5 (select |v_#memory_$Pointer$.base_58_const_-475207601| |v_~#m_inode~0.base_7_const_-469204139|)) (.cse0 (select |v_#memory_int_73_const_1545201429| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647|)) (.cse25 (+ |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_6_const_-1991001923| 64)) (.cse28 (+ |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_6_const_-1991001923| 40)) (.cse31 (+ |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_6_const_-1991001923| 56)) (.cse1 (+ |v_~#__CS_thread_lockedon~0.offset_5_const_541011271| 32)) (.cse33 (+ |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_6_const_-1991001923| 32)) (.cse35 (+ |v_~#__CS_thread_lockedon~0.offset_5_const_541011271| 48)) (.cse36 (+ |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_6_const_-1991001923| 48)) (.cse38 (+ |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_6_const_-1991001923| 24)) (.cse10 (select |v_#memory_$Pointer$.offset_60_const_-436731494| |v_~#inode~0.base_6_const_2075872712|)) (.cse7 (select |v_#memory_$Pointer$.base_73_const_-475207674| |v_~#__CS_thread_status~0.base_4_const_-48473261|)) (.cse2 (select |v_#memory_int_72_const_1545201418| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647|)) (.cse30 (+ |v_~#__CS_thread_lockedon~0.offset_5_const_541011271| 56)) (.cse48 (select |v_#memory_$Pointer$.base_74_const_-475207679| |v_~#__CS_thread_status~0.base_4_const_-48473261|)) (.cse52 (select |v_#memory_$Pointer$.base_56_const_-475207603| |v_~#m_busy~0.base_9_const_717935425|)) (.cse50 (select |v_#memory_$Pointer$.base_62_const_-475207578| |v_~#busy~0.base_6_const_-862540142|)) (.cse53 (select |v_#memory_$Pointer$.base_60_const_-475207580| |v_~#inode~0.base_6_const_2075872712|)) (.cse51 (select |v_#memory_int_71_const_1545201419| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647|)) (.cse27 (+ |v_~#__CS_thread_lockedon~0.offset_5_const_541011271| 40)) (.cse4 (+ |v_~#m_busy~0.offset_9_const_-527293729| 2)) (.cse11 (+ |v_~#inode~0.offset_6_const_-1342747578| 8)) (.cse47 (+ |v_~#inode~0.offset_6_const_-1342747578| 4)) (.cse49 (+ |v_~#busy~0.offset_6_const_1056451216| 4)) (.cse21 (+ |v_~#block~0.offset_7_const_283662439| 4)) (.cse17 (select |v_#memory_$Pointer$.offset_73_const_-436731580| |v_~#__CS_thread_status~0.base_4_const_-48473261|)) (.cse58 (select |v_#memory_$Pointer$.offset_72_const_-436731579| |v_~#__CS_thread_status~0.base_4_const_-48473261|)) (.cse60 (select |v_#memory_int_70_const_1545201416| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647|)) (.cse24 (+ |v_~#__CS_thread_lockedon~0.offset_5_const_541011271| 64)) (.cse12 (select |v_#memory_$Pointer$.offset_76_const_-436731583| |v_~#__CS_thread_status~0.base_4_const_-48473261|)) (.cse6 (+ |v_~#m_inode~0.offset_7_const_1100766803| 2)) (.cse3 (select |v_#memory_$Pointer$.offset_56_const_-436731517| |v_~#m_busy~0.base_9_const_717935425|)) (.cse56 (+ |v_~#m_busy~0.offset_9_const_-527293729| 1)) (.cse14 (select |v_#memory_$Pointer$.offset_75_const_-436731578| |v_~#__CS_thread_status~0.base_4_const_-48473261|)) (.cse15 (select |v_#memory_$Pointer$.offset_74_const_-436731577| |v_~#__CS_thread_status~0.base_4_const_-48473261|)) (.cse59 (select |v_#memory_$Pointer$.offset_62_const_-436731484| |v_~#busy~0.base_6_const_-862540142|)) (.cse57 (+ |v_~#busy~0.offset_6_const_1056451216| 8)) (.cse22 (select |v_#memory_$Pointer$.offset_64_const_-436731482| |v_~#block~0.base_7_const_-1770608023|)) (.cse41 (select |v_#memory_$Pointer$.base_64_const_-475207584| |v_~#block~0.base_7_const_-1770608023|)) (.cse73 (+ |v_~#block~0.offset_7_const_283662439| 8)) (.cse76 (select |v_#memory_$Pointer$.base_76_const_-475207677| |v_~#__CS_thread_status~0.base_4_const_-48473261|)) (.cse54 (select |v_#memory_$Pointer$.base_75_const_-475207680| |v_~#__CS_thread_status~0.base_4_const_-48473261|)) (.cse39 (select |v_#memory_int_74_const_1545201428| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647|)) (.cse37 (+ |v_~#__CS_thread_lockedon~0.offset_5_const_541011271| 24)) (.cse18 (+ |v_~#__CS_thread_status~0.offset_4_const_1684530065| 8)) (.cse8 (+ |v_~#__CS_thread_status~0.offset_4_const_1684530065| 5)) (.cse16 (+ |v_~#__CS_thread_status~0.offset_4_const_1684530065| 7)) (.cse55 (+ |v_~#__CS_thread_status~0.offset_4_const_1684530065| 4)) (.cse13 (+ |v_~#__CS_thread_status~0.offset_4_const_1684530065| 6)) (.cse74 (+ |v_~#__CS_thread_status~0.offset_4_const_1684530065| 3)) (.cse75 (select |v_#memory_$Pointer$.offset_58_const_-436731507| |v_~#m_inode~0.base_7_const_-469204139|)) (.cse19 (+ |v_~#m_inode~0.offset_7_const_1100766803| 1))) (and (= (store |v_#memory_int_73_const_1545201429| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| (store .cse0 .cse1 (select .cse2 .cse1))) |v_#memory_int_72_const_1545201418|) (= (store |v_#memory_$Pointer$.offset_56_const_-436731517| |v_~#m_busy~0.base_9_const_717935425| (store .cse3 .cse4 (select (select |v_#memory_$Pointer$.offset_55_const_-436731520| |v_~#m_busy~0.base_9_const_717935425|) .cse4))) |v_#memory_$Pointer$.offset_55_const_-436731520|) (= |v_#memory_$Pointer$.base_57_const_-475207604| (store |v_#memory_$Pointer$.base_58_const_-475207601| |v_~#m_inode~0.base_7_const_-469204139| (store .cse5 .cse6 (select (select |v_#memory_$Pointer$.base_57_const_-475207604| |v_~#m_inode~0.base_7_const_-469204139|) .cse6)))) (= (store |v_#memory_$Pointer$.base_73_const_-475207674| |v_~#__CS_thread_status~0.base_4_const_-48473261| (store .cse7 .cse8 (select .cse9 .cse8))) |v_#memory_$Pointer$.base_72_const_-475207673|) (= |v_#memory_$Pointer$.offset_59_const_-436731508| (store |v_#memory_$Pointer$.offset_60_const_-436731494| |v_~#inode~0.base_6_const_2075872712| (store .cse10 .cse11 (select (select |v_#memory_$Pointer$.offset_59_const_-436731508| |v_~#inode~0.base_6_const_2075872712|) .cse11)))) (= (store |v_#memory_$Pointer$.offset_76_const_-436731583| |v_~#__CS_thread_status~0.base_4_const_-48473261| (store .cse12 .cse13 (select .cse14 .cse13))) |v_#memory_$Pointer$.offset_75_const_-436731578|) (= |v_#memory_$Pointer$.offset_73_const_-436731580| (store |v_#memory_$Pointer$.offset_74_const_-436731577| |v_~#__CS_thread_status~0.base_4_const_-48473261| (store .cse15 .cse16 (select .cse17 .cse16)))) (= |v_#memory_$Pointer$.base_71_const_-475207676| (store |v_#memory_$Pointer$.base_72_const_-475207673| |v_~#__CS_thread_status~0.base_4_const_-48473261| (store .cse9 .cse18 (select (select |v_#memory_$Pointer$.base_71_const_-475207676| |v_~#__CS_thread_status~0.base_4_const_-48473261|) .cse18)))) (= |v_#memory_$Pointer$.base_58_const_-475207601| (store |v_#memory_$Pointer$.base_59_const_-475207602| |v_~#m_inode~0.base_7_const_-469204139| (store (select |v_#memory_$Pointer$.base_59_const_-475207602| |v_~#m_inode~0.base_7_const_-469204139|) .cse19 (select .cse5 .cse19)))) (= (store |v_#memory_$Pointer$.base_53_const_-475207616| |v_~#__CS_thread_allocated~0.base_3_const_1055191041| (store (select |v_#memory_$Pointer$.base_53_const_-475207616| |v_~#__CS_thread_allocated~0.base_3_const_1055191041|) |v_~#__CS_thread_allocated~0.offset_3_const_1454422303| (select (select |v_#memory_$Pointer$.base_52_const_-475207615| |v_~#__CS_thread_allocated~0.base_3_const_1055191041|) |v_~#__CS_thread_allocated~0.offset_3_const_1454422303|))) |v_#memory_$Pointer$.base_52_const_-475207615|) (= (let ((.cse20 (store |v_#memory_$Pointer$.offset_71_const_-436731462| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| (let ((.cse23 (let ((.cse26 (let ((.cse29 (let ((.cse32 (let ((.cse34 (store (select |v_#memory_$Pointer$.offset_71_const_-436731462| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647|) .cse37 (select (select |v_#memory_$Pointer$.offset_71_const_-436731462| |v_main_~#__CS_cp___CS_thread_lockedon~0.base_6_const_-1933732865|) .cse38)))) (store .cse34 .cse35 (select (select (store |v_#memory_$Pointer$.offset_71_const_-436731462| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| .cse34) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_6_const_-1933732865|) .cse36))))) (store .cse32 .cse1 (select (select (store |v_#memory_$Pointer$.offset_71_const_-436731462| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| .cse32) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_6_const_-1933732865|) .cse33))))) (store .cse29 .cse30 (select (select (store |v_#memory_$Pointer$.offset_71_const_-436731462| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| .cse29) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_6_const_-1933732865|) .cse31))))) (store .cse26 .cse27 (select (select (store |v_#memory_$Pointer$.offset_71_const_-436731462| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| .cse26) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_6_const_-1933732865|) .cse28))))) (store .cse23 .cse24 (select (select (store |v_#memory_$Pointer$.offset_71_const_-436731462| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| .cse23) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_6_const_-1933732865|) .cse25)))))) (store .cse20 |v_~#block~0.base_7_const_-1770608023| (store (select .cse20 |v_~#block~0.base_7_const_-1770608023|) .cse21 (select .cse22 .cse21)))) |v_#memory_$Pointer$.offset_64_const_-436731482|) (= |v_#memory_int_73_const_1545201429| (store |v_#memory_int_74_const_1545201428| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| (store .cse39 .cse35 (select .cse0 .cse35)))) (= (store |v_#memory_$Pointer$.offset_55_const_-436731520| |v_~#__CS_thread_born_round~0.base_3_const_1720302586| (store (select |v_#memory_$Pointer$.offset_55_const_-436731520| |v_~#__CS_thread_born_round~0.base_3_const_1720302586|) |v_~#__CS_thread_born_round~0.offset_3_const_544850616| (select (select |v_#memory_$Pointer$.offset_54_const_-436731519| |v_~#__CS_thread_born_round~0.base_3_const_1720302586|) |v_~#__CS_thread_born_round~0.offset_3_const_544850616|))) |v_#memory_$Pointer$.offset_54_const_-436731519|) (= |v_#memory_$Pointer$.base_64_const_-475207584| (let ((.cse40 (store |v_#memory_$Pointer$.base_71_const_-475207676| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| (let ((.cse42 (let ((.cse43 (let ((.cse44 (let ((.cse45 (let ((.cse46 (store (select |v_#memory_$Pointer$.base_71_const_-475207676| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647|) .cse37 (select (select |v_#memory_$Pointer$.base_71_const_-475207676| |v_main_~#__CS_cp___CS_thread_lockedon~0.base_6_const_-1933732865|) .cse38)))) (store .cse46 .cse35 (select (select (store |v_#memory_$Pointer$.base_71_const_-475207676| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| .cse46) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_6_const_-1933732865|) .cse36))))) (store .cse45 .cse1 (select (select (store |v_#memory_$Pointer$.base_71_const_-475207676| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| .cse45) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_6_const_-1933732865|) .cse33))))) (store .cse44 .cse30 (select (select (store |v_#memory_$Pointer$.base_71_const_-475207676| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| .cse44) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_6_const_-1933732865|) .cse31))))) (store .cse43 .cse27 (select (select (store |v_#memory_$Pointer$.base_71_const_-475207676| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| .cse43) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_6_const_-1933732865|) .cse28))))) (store .cse42 .cse24 (select (select (store |v_#memory_$Pointer$.base_71_const_-475207676| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| .cse42) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_6_const_-1933732865|) .cse25)))))) (store .cse40 |v_~#block~0.base_7_const_-1770608023| (store (select .cse40 |v_~#block~0.base_7_const_-1770608023|) .cse21 (select .cse41 .cse21))))) (= (store |v_#memory_$Pointer$.offset_61_const_-436731483| |v_~#inode~0.base_6_const_2075872712| (store (select |v_#memory_$Pointer$.offset_61_const_-436731483| |v_~#inode~0.base_6_const_2075872712|) .cse47 (select .cse10 .cse47))) |v_#memory_$Pointer$.offset_60_const_-436731494|) (= |v_#memory_$Pointer$.base_73_const_-475207674| (store |v_#memory_$Pointer$.base_74_const_-475207679| |v_~#__CS_thread_status~0.base_4_const_-48473261| (store .cse48 .cse16 (select .cse7 .cse16)))) (= |v_#memory_$Pointer$.base_62_const_-475207578| (store |v_#memory_$Pointer$.base_63_const_-475207583| |v_~#busy~0.base_6_const_-862540142| (store (select |v_#memory_$Pointer$.base_63_const_-475207583| |v_~#busy~0.base_6_const_-862540142|) .cse49 (select .cse50 .cse49)))) (= (store |v_#memory_$Pointer$.offset_54_const_-436731519| |v_~#__CS_thread_status~0.base_4_const_-48473261| (store (select |v_#memory_$Pointer$.offset_54_const_-436731519| |v_~#__CS_thread_status~0.base_4_const_-48473261|) |v_~#__CS_thread_status~0.offset_4_const_1684530065| (select (select |v_#memory_$Pointer$.offset_53_const_-436731514| |v_~#__CS_thread_status~0.base_4_const_-48473261|) |v_~#__CS_thread_status~0.offset_4_const_1684530065|))) |v_#memory_$Pointer$.offset_53_const_-436731514|) (= (store |v_#memory_int_72_const_1545201418| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| (store .cse2 .cse30 (select .cse51 .cse30))) |v_#memory_int_71_const_1545201419|) (= |v_#memory_$Pointer$.base_55_const_-475207614| (store |v_#memory_$Pointer$.base_56_const_-475207603| |v_~#m_busy~0.base_9_const_717935425| (store .cse52 .cse4 (select (select |v_#memory_$Pointer$.base_55_const_-475207614| |v_~#m_busy~0.base_9_const_717935425|) .cse4)))) (= |v_#memory_$Pointer$.offset_52_const_-436731513| (store |v_#memory_$Pointer$.offset_53_const_-436731514| |v_~#__CS_thread_allocated~0.base_3_const_1055191041| (store (select |v_#memory_$Pointer$.offset_53_const_-436731514| |v_~#__CS_thread_allocated~0.base_3_const_1055191041|) |v_~#__CS_thread_allocated~0.offset_3_const_1454422303| (select (select |v_#memory_$Pointer$.offset_52_const_-436731513| |v_~#__CS_thread_allocated~0.base_3_const_1055191041|) |v_~#__CS_thread_allocated~0.offset_3_const_1454422303|)))) (= v_~__CS_round~0_91_const_-563051970 0) (= |v_main_#t~mem77_1_const_204397592| (select (select |v_#memory_int_56_const_1545201488| |v_~#__CS_thread_allocated~0.base_3_const_1055191041|) |v_~#__CS_thread_allocated~0.offset_3_const_1454422303|)) (= |v_#memory_$Pointer$.base_54_const_-475207613| (store |v_#memory_$Pointer$.base_55_const_-475207614| |v_~#__CS_thread_born_round~0.base_3_const_1720302586| (store (select |v_#memory_$Pointer$.base_55_const_-475207614| |v_~#__CS_thread_born_round~0.base_3_const_1720302586|) |v_~#__CS_thread_born_round~0.offset_3_const_544850616| (select (select |v_#memory_$Pointer$.base_54_const_-475207613| |v_~#__CS_thread_born_round~0.base_3_const_1720302586|) |v_~#__CS_thread_born_round~0.offset_3_const_544850616|)))) (= (store |v_#memory_$Pointer$.base_60_const_-475207580| |v_~#inode~0.base_6_const_2075872712| (store .cse53 .cse11 (select (select |v_#memory_$Pointer$.base_59_const_-475207602| |v_~#inode~0.base_6_const_2075872712|) .cse11))) |v_#memory_$Pointer$.base_59_const_-475207602|) (= |v_#memory_$Pointer$.base_74_const_-475207679| (store |v_#memory_$Pointer$.base_75_const_-475207680| |v_~#__CS_thread_status~0.base_4_const_-48473261| (store .cse54 .cse55 (select .cse48 .cse55)))) (= v_~__CS_thread~0.base_11_const_-335877311 (store v_~__CS_thread~0.base_12_const_-335877312 0 |#funAddr~main_thread.base|)) (= |v_#memory_$Pointer$.base_56_const_-475207603| (store |v_#memory_$Pointer$.base_57_const_-475207604| |v_~#m_busy~0.base_9_const_717935425| (store (select |v_#memory_$Pointer$.base_57_const_-475207604| |v_~#m_busy~0.base_9_const_717935425|) .cse56 (select .cse52 .cse56)))) (= v_~__CS_thread_index~0_8_const_-147234547 0) (= |v_#memory_$Pointer$.base_61_const_-475207577| (store |v_#memory_$Pointer$.base_62_const_-475207578| |v_~#busy~0.base_6_const_-862540142| (store .cse50 .cse57 (select (select |v_#memory_$Pointer$.base_61_const_-475207577| |v_~#busy~0.base_6_const_-862540142|) .cse57)))) (= (store |v_#memory_$Pointer$.offset_72_const_-436731579| |v_~#__CS_thread_status~0.base_4_const_-48473261| (store .cse58 .cse18 (select (select |v_#memory_$Pointer$.offset_71_const_-436731462| |v_~#__CS_thread_status~0.base_4_const_-48473261|) .cse18))) |v_#memory_$Pointer$.offset_71_const_-436731462|) (= |v_#memory_$Pointer$.offset_62_const_-436731484| (store |v_#memory_$Pointer$.offset_63_const_-436731481| |v_~#busy~0.base_6_const_-862540142| (store (select |v_#memory_$Pointer$.offset_63_const_-436731481| |v_~#busy~0.base_6_const_-862540142|) .cse49 (select .cse59 .cse49)))) (= (store |v_#memory_$Pointer$.base_61_const_-475207577| |v_~#inode~0.base_6_const_2075872712| (store (select |v_#memory_$Pointer$.base_61_const_-475207577| |v_~#inode~0.base_6_const_2075872712|) .cse47 (select .cse53 .cse47))) |v_#memory_$Pointer$.base_60_const_-475207580|) (= (store |v_#memory_int_71_const_1545201419| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| (store .cse51 .cse27 (select .cse60 .cse27))) |v_#memory_int_70_const_1545201416|) (= (let ((.cse61 (let ((.cse62 (let ((.cse63 (let ((.cse64 (let ((.cse66 (let ((.cse68 (let ((.cse70 (store |v_#memory_int_69_const_1545201522| |v_~#block~0.base_7_const_-1770608023| (let ((.cse72 (store (select |v_#memory_int_69_const_1545201522| |v_~#block~0.base_7_const_-1770608023|) .cse21 (select (select |v_#memory_int_69_const_1545201522| |v_main_~#__CS_cp_block~0.base_6_const_304370259|) (+ |v_main_~#__CS_cp_block~0.offset_6_const_1469162001| 4))))) (store .cse72 .cse73 (select (select (store |v_#memory_int_69_const_1545201522| |v_~#block~0.base_7_const_-1770608023| .cse72) |v_main_~#__CS_cp_block~0.base_6_const_304370259|) (+ |v_main_~#__CS_cp_block~0.offset_6_const_1469162001| 8))))))) (store .cse70 |v_~#busy~0.base_6_const_-862540142| (let ((.cse71 (store (select .cse70 |v_~#busy~0.base_6_const_-862540142|) .cse49 (select (select .cse70 |v_main_~#__CS_cp_busy~0.base_6_const_728408393|) (+ |v_main_~#__CS_cp_busy~0.offset_6_const_956269447| 4))))) (store .cse71 .cse57 (select (select (store .cse70 |v_~#busy~0.base_6_const_-862540142| .cse71) |v_main_~#__CS_cp_busy~0.base_6_const_728408393|) (+ |v_main_~#__CS_cp_busy~0.offset_6_const_956269447| 8)))))))) (store .cse68 |v_~#inode~0.base_6_const_2075872712| (let ((.cse69 (store (select .cse68 |v_~#inode~0.base_6_const_2075872712|) .cse47 (select (select .cse68 |v_main_~#__CS_cp_inode~0.base_6_const_-144247247|) (+ |v_main_~#__CS_cp_inode~0.offset_6_const_-157493745| 4))))) (store .cse69 .cse11 (select (select (store .cse68 |v_~#inode~0.base_6_const_2075872712| .cse69) |v_main_~#__CS_cp_inode~0.base_6_const_-144247247|) (+ |v_main_~#__CS_cp_inode~0.offset_6_const_-157493745| 8)))))))) (store .cse66 |v_~#m_inode~0.base_7_const_-469204139| (let ((.cse67 (store (select .cse66 |v_~#m_inode~0.base_7_const_-469204139|) .cse19 (select (select .cse66 |v_main_~#__CS_cp_m_inode~0.base_6_const_716180767|) (+ |v_main_~#__CS_cp_m_inode~0.offset_6_const_2084641245| 1))))) (store .cse67 .cse6 (select (select (store .cse66 |v_~#m_inode~0.base_7_const_-469204139| .cse67) |v_main_~#__CS_cp_m_inode~0.base_6_const_716180767|) (+ |v_main_~#__CS_cp_m_inode~0.offset_6_const_2084641245| 2)))))))) (store .cse64 |v_~#m_busy~0.base_9_const_717935425| (let ((.cse65 (store (select .cse64 |v_~#m_busy~0.base_9_const_717935425|) .cse56 (select (select .cse64 |v_main_~#__CS_cp_m_busy~0.base_6_const_617622715|) (+ |v_main_~#__CS_cp_m_busy~0.offset_6_const_1859883641| 1))))) (store .cse65 .cse4 (select (select (store .cse64 |v_~#m_busy~0.base_9_const_717935425| .cse65) |v_main_~#__CS_cp_m_busy~0.base_6_const_617622715|) (+ |v_main_~#__CS_cp_m_busy~0.offset_6_const_1859883641| 2)))))))) (store .cse63 |v_~#__CS_thread_born_round~0.base_3_const_1720302586| (store (select .cse63 |v_~#__CS_thread_born_round~0.base_3_const_1720302586|) |v_~#__CS_thread_born_round~0.offset_3_const_544850616| v_~__CS_round~0_91_const_-563051970))))) (store .cse62 |v_~#__CS_thread_status~0.base_4_const_-48473261| (store (select .cse62 |v_~#__CS_thread_status~0.base_4_const_-48473261|) |v_~#__CS_thread_status~0.offset_4_const_1684530065| v_~__THREAD_RUNNING~0_2_const_278392747))))) (store .cse61 |v_~#__CS_thread_allocated~0.base_3_const_1055191041| (store (select .cse61 |v_~#__CS_thread_allocated~0.base_3_const_1055191041|) |v_~#__CS_thread_allocated~0.offset_3_const_1454422303| 1))) |v_#memory_int_56_const_1545201488|) (= |v_#memory_$Pointer$.offset_72_const_-436731579| (store |v_#memory_$Pointer$.offset_73_const_-436731580| |v_~#__CS_thread_status~0.base_4_const_-48473261| (store .cse17 .cse8 (select .cse58 .cse8)))) (= (store |v_#memory_int_70_const_1545201416| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| (store .cse60 .cse24 (select (select |v_#memory_int_69_const_1545201522| |v_~#__CS_thread_lockedon~0.base_5_const_-898830647|) .cse24))) |v_#memory_int_69_const_1545201522|) (= (store |v_#memory_$Pointer$.offset_77_const_-436731584| |v_~#__CS_thread_status~0.base_4_const_-48473261| (store (select |v_#memory_$Pointer$.offset_77_const_-436731584| |v_~#__CS_thread_status~0.base_4_const_-48473261|) .cse74 (select .cse12 .cse74))) |v_#memory_$Pointer$.offset_76_const_-436731583|) (= (store |v_#memory_$Pointer$.offset_58_const_-436731507| |v_~#m_inode~0.base_7_const_-469204139| (store .cse75 .cse6 (select (select |v_#memory_$Pointer$.offset_57_const_-436731518| |v_~#m_inode~0.base_7_const_-469204139|) .cse6))) |v_#memory_$Pointer$.offset_57_const_-436731518|) (= |v_#memory_$Pointer$.offset_56_const_-436731517| (store |v_#memory_$Pointer$.offset_57_const_-436731518| |v_~#m_busy~0.base_9_const_717935425| (store (select |v_#memory_$Pointer$.offset_57_const_-436731518| |v_~#m_busy~0.base_9_const_717935425|) .cse56 (select .cse3 .cse56)))) (= |v_#memory_$Pointer$.offset_74_const_-436731577| (store |v_#memory_$Pointer$.offset_75_const_-436731578| |v_~#__CS_thread_status~0.base_4_const_-48473261| (store .cse14 .cse55 (select .cse15 .cse55)))) (= (store |v_#memory_$Pointer$.offset_62_const_-436731484| |v_~#busy~0.base_6_const_-862540142| (store .cse59 .cse57 (select (select |v_#memory_$Pointer$.offset_61_const_-436731483| |v_~#busy~0.base_6_const_-862540142|) .cse57))) |v_#memory_$Pointer$.offset_61_const_-436731483|) (= |v_#memory_$Pointer$.base_76_const_-475207677| (store |v_#memory_$Pointer$.base_77_const_-475207678| |v_~#__CS_thread_status~0.base_4_const_-48473261| (store (select |v_#memory_$Pointer$.base_77_const_-475207678| |v_~#__CS_thread_status~0.base_4_const_-48473261|) .cse74 (select .cse76 .cse74)))) (= |v_#memory_$Pointer$.offset_63_const_-436731481| (store |v_#memory_$Pointer$.offset_64_const_-436731482| |v_~#block~0.base_7_const_-1770608023| (store .cse22 .cse73 (select (select |v_#memory_$Pointer$.offset_63_const_-436731481| |v_~#block~0.base_7_const_-1770608023|) .cse73)))) (= (store |v_#memory_$Pointer$.base_54_const_-475207613| |v_~#__CS_thread_status~0.base_4_const_-48473261| (store (select |v_#memory_$Pointer$.base_54_const_-475207613| |v_~#__CS_thread_status~0.base_4_const_-48473261|) |v_~#__CS_thread_status~0.offset_4_const_1684530065| (select (select |v_#memory_$Pointer$.base_53_const_-475207616| |v_~#__CS_thread_status~0.base_4_const_-48473261|) |v_~#__CS_thread_status~0.offset_4_const_1684530065|))) |v_#memory_$Pointer$.base_53_const_-475207616|) (= (store |v_#memory_$Pointer$.base_64_const_-475207584| |v_~#block~0.base_7_const_-1770608023| (store .cse41 .cse73 (select (select |v_#memory_$Pointer$.base_63_const_-475207583| |v_~#block~0.base_7_const_-1770608023|) .cse73))) |v_#memory_$Pointer$.base_63_const_-475207583|) (= v_~__CS_thread~0.offset_11_const_1266608195 (store v_~__CS_thread~0.offset_12_const_1266608194 0 |#funAddr~main_thread.offset|)) (= (store |v_#memory_$Pointer$.base_76_const_-475207677| |v_~#__CS_thread_status~0.base_4_const_-48473261| (store .cse76 .cse13 (select .cse54 .cse13))) |v_#memory_$Pointer$.base_75_const_-475207680|) (= (let ((.cse77 (store |v_#memory_int_81_const_1545201448| |v_~#__CS_thread_status~0.base_4_const_-48473261| (let ((.cse78 (let ((.cse79 (let ((.cse80 (let ((.cse81 (let ((.cse82 (store (select |v_#memory_int_81_const_1545201448| |v_~#__CS_thread_status~0.base_4_const_-48473261|) .cse74 (select (select |v_#memory_int_81_const_1545201448| |v_main_~#__CS_cp___CS_thread_status~0.base_6_const_1635486152|) (+ |v_main_~#__CS_cp___CS_thread_status~0.offset_6_const_649365574| 3))))) (store .cse82 .cse13 (select (select (store |v_#memory_int_81_const_1545201448| |v_~#__CS_thread_status~0.base_4_const_-48473261| .cse82) |v_main_~#__CS_cp___CS_thread_status~0.base_6_const_1635486152|) (+ |v_main_~#__CS_cp___CS_thread_status~0.offset_6_const_649365574| 6)))))) (store .cse81 .cse55 (select (select (store |v_#memory_int_81_const_1545201448| |v_~#__CS_thread_status~0.base_4_const_-48473261| .cse81) |v_main_~#__CS_cp___CS_thread_status~0.base_6_const_1635486152|) (+ |v_main_~#__CS_cp___CS_thread_status~0.offset_6_const_649365574| 4)))))) (store .cse80 .cse16 (select (select (store |v_#memory_int_81_const_1545201448| |v_~#__CS_thread_status~0.base_4_const_-48473261| .cse80) |v_main_~#__CS_cp___CS_thread_status~0.base_6_const_1635486152|) (+ |v_main_~#__CS_cp___CS_thread_status~0.offset_6_const_649365574| 7)))))) (store .cse79 .cse8 (select (select (store |v_#memory_int_81_const_1545201448| |v_~#__CS_thread_status~0.base_4_const_-48473261| .cse79) |v_main_~#__CS_cp___CS_thread_status~0.base_6_const_1635486152|) (+ |v_main_~#__CS_cp___CS_thread_status~0.offset_6_const_649365574| 5)))))) (store .cse78 .cse18 (select (select (store |v_#memory_int_81_const_1545201448| |v_~#__CS_thread_status~0.base_4_const_-48473261| .cse78) |v_main_~#__CS_cp___CS_thread_status~0.base_6_const_1635486152|) (+ |v_main_~#__CS_cp___CS_thread_status~0.offset_6_const_649365574| 8))))))) (store .cse77 |v_~#__CS_thread_lockedon~0.base_5_const_-898830647| (store (select .cse77 |v_~#__CS_thread_lockedon~0.base_5_const_-898830647|) .cse37 (select .cse39 .cse37)))) |v_#memory_int_74_const_1545201428|) (= |v_#memory_$Pointer$.offset_58_const_-436731507| (store |v_#memory_$Pointer$.offset_59_const_-436731508| |v_~#m_inode~0.base_7_const_-469204139| (store (select |v_#memory_$Pointer$.offset_59_const_-436731508| |v_~#m_inode~0.base_7_const_-469204139|) .cse19 (select .cse75 .cse19)))))))
(check-sat)
(exit)