cs_peterson_true-unreach-call.i_0.smt2 32.2 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
(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~thr1.base| () Int)
(declare-fun |#funAddr~thr1.offset| () Int)
(declare-fun |#funAddr~thr2.base| () Int)
(declare-fun |#funAddr~thr2.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 (= |#funAddr~thr1.offset| 0) (= (- 1) |#funAddr~thr1.base|)))
(assert (and (= (- 1) |#funAddr~thr2.base|) (= 1 |#funAddr~thr2.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_47_const_1545201586| () (Array Int (Array Int Int)))
(declare-fun |v_main_~#__CS_cp_flag1~0.base_1_const_685083920| () Int)
(declare-fun |v_main_~#__CS_cp_flag1~0.offset_1_const_2139279086| () Int)
(declare-fun |v_~#flag1~0.base_5_const_-1389894365| () Int)
(declare-fun |v_~#flag1~0.offset_5_const_954025249| () Int)
(declare-fun |v_main_~#__CS_cp_flag2~0.base_1_const_488578097| () Int)
(declare-fun |v_main_~#__CS_cp_flag2~0.offset_1_const_-2026608305| () Int)
(declare-fun |v_~#flag2~0.base_5_const_-1586400316| () Int)
(declare-fun |v_~#flag2~0.offset_5_const_1083121538| () Int)
(declare-fun |v_main_~#__CS_cp_turn~0.base_1_const_-594232398| () Int)
(declare-fun |v_main_~#__CS_cp_turn~0.offset_1_const_1195896048| () Int)
(declare-fun |v_~#turn~0.base_6_const_2109769878| () Int)
(declare-fun |v_~#turn~0.offset_6_const_1296077716| () Int)
(declare-fun |v_main_~#__CS_cp_x~0.base_1_const_-969430205| () Int)
(declare-fun |v_main_~#__CS_cp_x~0.offset_1_const_1290085441| () Int)
(declare-fun |v_~#x~0.base_6_const_-402024747| () Int)
(declare-fun |v_~#x~0.offset_6_const_1100090899| () Int)
(declare-fun |v_~#__CS_thread_born_round~0.base_2_const_1720302587| () Int)
(declare-fun |v_~#__CS_thread_born_round~0.offset_2_const_544850617| () Int)
(declare-fun v_~__CS_round~0_72_const_-563051909 () Int)
(declare-fun |v_~#__CS_thread_status~0.base_2_const_-48473259| () Int)
(declare-fun |v_~#__CS_thread_status~0.offset_2_const_1684530067| () Int)
(declare-fun v_~__THREAD_RUNNING~0_2_const_278392747 () Int)
(declare-fun |v_~#__CS_thread_allocated~0.base_2_const_1055191042| () Int)
(declare-fun |v_~#__CS_thread_allocated~0.offset_2_const_1454422272| () Int)
(declare-fun |v_#memory_int_36_const_1545201554| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_50_const_1545201482| () (Array Int (Array Int Int)))
(declare-fun |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| () Int)
(declare-fun |v_~#__CS_thread_lockedon~0.offset_4_const_541011272| () Int)
(declare-fun |v_#memory_int_51_const_1545201493| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_51_const_-475207610| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_52_const_-475207615| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_52_const_1545201492| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_30_const_-475207551| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_31_const_-475207552| () (Array Int (Array Int Int)))
(declare-fun v_~__CS_thread~0.base_9_const_-308947756 () (Array Int Int))
(declare-fun v_~__CS_thread~0.base_10_const_-335877310 () (Array Int Int))
(declare-fun |v_#memory_$Pointer$.base_36_const_-475207537| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_37_const_-475207538| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_47_const_-475207505| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_48_const_-475207506| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_30_const_-436731449| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_31_const_-436731450| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_48_const_-436731412| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_49_const_-436731409| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_33_const_-475207550| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_34_const_-475207539| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_34_const_-436731453| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_35_const_-436731454| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_46_const_-436731422| () (Array Int (Array Int Int)))
(declare-fun |v_main_~#__CS_cp___CS_thread_lockedon~0.base_2_const_-1933732893| () Int)
(declare-fun |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_2_const_-1991001951| () Int)
(declare-fun |v_#memory_$Pointer$.offset_39_const_-436731442| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_32_const_-436731455| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_32_const_-475207549| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_29_const_-436731863| () (Array Int (Array Int Int)))
(declare-fun |v_main_#t~mem66_1_const_204362872| () Int)
(declare-fun |v_#memory_$Pointer$.base_50_const_-475207609| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_33_const_-436731456| () (Array Int (Array Int Int)))
(declare-fun v_~__CS_thread_index~0_6_const_-147234545 () Int)
(declare-fun |v_#memory_int_48_const_1545201597| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_37_const_-436731444| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_38_const_-436731441| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_50_const_-436731515| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_35_const_-475207540| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_36_const_-436731443| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_59_const_1545201501| () (Array Int (Array Int Int)))
(declare-fun |v_main_~#__CS_cp___CS_thread_status~0.base_2_const_1635486156| () Int)
(declare-fun |v_main_~#__CS_cp___CS_thread_status~0.offset_2_const_649365578| () Int)
(declare-fun |v_#memory_$Pointer$.base_46_const_-475207508| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_49_const_-475207511| () (Array Int (Array Int Int)))
(declare-fun v_~__CS_thread~0.offset_9_const_-97333358 () (Array Int Int))
(declare-fun v_~__CS_thread~0.offset_10_const_1266608196 () (Array Int Int))
(declare-fun |v_#memory_$Pointer$.offset_51_const_-436731516| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_47_const_-436731411| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_38_const_-475207543| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_39_const_-475207544| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_29_const_-475207445| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_49_const_1545201596| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_52_const_-436731513| () (Array Int (Array Int Int)))
(assert (let ((.cse0 (select |v_#memory_int_51_const_1545201493| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646|)) (.cse4 (select |v_#memory_$Pointer$.base_51_const_-475207610| |v_~#__CS_thread_status~0.base_2_const_-48473259|)) (.cse12 (select |v_#memory_$Pointer$.offset_49_const_-436731409| |v_~#__CS_thread_status~0.base_2_const_-48473259|)) (.cse39 (select |v_#memory_$Pointer$.offset_33_const_-436731456| |v_~#x~0.base_6_const_-402024747|)) (.cse21 (select |v_#memory_$Pointer$.offset_39_const_-436731442| |v_~#flag1~0.base_5_const_-1389894365|)) (.cse43 (select |v_#memory_$Pointer$.offset_37_const_-436731444| |v_~#flag2~0.base_5_const_-1586400316|)) (.cse5 (select |v_#memory_int_52_const_1545201492| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646|)) (.cse11 (select |v_#memory_$Pointer$.base_47_const_-475207505| |v_~#__CS_thread_status~0.base_2_const_-48473259|)) (.cse38 (select |v_#memory_$Pointer$.base_50_const_-475207609| |v_~#__CS_thread_status~0.base_2_const_-48473259|)) (.cse45 (+ |v_~#__CS_thread_status~0.offset_2_const_1684530067| 4)) (.cse17 (select |v_#memory_$Pointer$.offset_35_const_-436731454| |v_~#turn~0.base_6_const_2109769878|)) (.cse44 (select |v_#memory_$Pointer$.offset_50_const_-436731515| |v_~#__CS_thread_status~0.base_2_const_-48473259|)) (.cse37 (+ |v_~#__CS_thread_status~0.offset_2_const_1684530067| 6)) (.cse51 (+ |v_~#__CS_thread_status~0.offset_2_const_1684530067| 8)) (.cse7 (select |v_#memory_$Pointer$.base_37_const_-475207538| |v_~#flag2~0.base_5_const_-1586400316|)) (.cse56 (select |v_#memory_$Pointer$.base_49_const_-475207511| |v_~#__CS_thread_status~0.base_2_const_-48473259|)) (.cse9 (select |v_#memory_$Pointer$.base_48_const_-475207506| |v_~#__CS_thread_status~0.base_2_const_-48473259|)) (.cse13 (+ |v_~#__CS_thread_status~0.offset_2_const_1684530067| 7)) (.cse41 (select |v_#memory_int_48_const_1545201597| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646|)) (.cse57 (select |v_#memory_$Pointer$.offset_51_const_-436731516| |v_~#__CS_thread_status~0.base_2_const_-48473259|)) (.cse3 (+ |v_~#__CS_thread_status~0.offset_2_const_1684530067| 3)) (.cse14 (select |v_#memory_$Pointer$.offset_48_const_-436731412| |v_~#__CS_thread_status~0.base_2_const_-48473259|)) (.cse58 (select |v_#memory_$Pointer$.offset_47_const_-436731411| |v_~#__CS_thread_status~0.base_2_const_-48473259|)) (.cse10 (+ |v_~#__CS_thread_status~0.offset_2_const_1684530067| 5)) (.cse2 (select |v_#memory_int_50_const_1545201482| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646|)) (.cse60 (select |v_#memory_int_49_const_1545201596| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646|)) (.cse15 (+ |v_~#x~0.offset_6_const_1100090899| 4)) (.cse46 (+ |v_~#turn~0.offset_6_const_1296077716| 4)) (.cse8 (+ |v_~#flag2~0.offset_5_const_1083121538| 8)) (.cse42 (+ |v_~#flag2~0.offset_5_const_1083121538| 4)) (.cse48 (+ |v_~#flag1~0.offset_5_const_954025249| 8)) (.cse47 (select |v_#memory_$Pointer$.base_35_const_-475207540| |v_~#turn~0.base_6_const_2109769878|)) (.cse18 (+ |v_~#turn~0.offset_6_const_1296077716| 8)) (.cse16 (select |v_#memory_$Pointer$.base_33_const_-475207550| |v_~#x~0.base_6_const_-402024747|)) (.cse40 (+ |v_~#x~0.offset_6_const_1100090899| 8)) (.cse59 (select |v_#memory_$Pointer$.base_39_const_-475207544| |v_~#flag1~0.base_5_const_-1389894365|)) (.cse20 (+ |v_~#flag1~0.offset_5_const_954025249| 4)) (.cse23 (+ |v_~#__CS_thread_lockedon~0.offset_4_const_541011272| 64)) (.cse24 (+ |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_2_const_-1991001951| 64)) (.cse26 (+ |v_~#__CS_thread_lockedon~0.offset_4_const_541011272| 40)) (.cse27 (+ |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_2_const_-1991001951| 40)) (.cse29 (+ |v_~#__CS_thread_lockedon~0.offset_4_const_541011272| 56)) (.cse30 (+ |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_2_const_-1991001951| 56)) (.cse1 (+ |v_~#__CS_thread_lockedon~0.offset_4_const_541011272| 32)) (.cse32 (+ |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_2_const_-1991001951| 32)) (.cse6 (+ |v_~#__CS_thread_lockedon~0.offset_4_const_541011272| 48)) (.cse34 (+ |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_2_const_-1991001951| 48)) (.cse35 (+ |v_~#__CS_thread_lockedon~0.offset_4_const_541011272| 24)) (.cse36 (+ |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_2_const_-1991001951| 24))) (and (= (store |v_#memory_int_51_const_1545201493| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| (store .cse0 .cse1 (select .cse2 .cse1))) |v_#memory_int_50_const_1545201482|) (= (store |v_#memory_$Pointer$.base_52_const_-475207615| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store (select |v_#memory_$Pointer$.base_52_const_-475207615| |v_~#__CS_thread_status~0.base_2_const_-48473259|) .cse3 (select .cse4 .cse3))) |v_#memory_$Pointer$.base_51_const_-475207610|) (= (store |v_#memory_int_52_const_1545201492| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| (store .cse5 .cse6 (select .cse0 .cse6))) |v_#memory_int_51_const_1545201493|) (= |v_#memory_$Pointer$.base_30_const_-475207551| (store |v_#memory_$Pointer$.base_31_const_-475207552| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store (select |v_#memory_$Pointer$.base_31_const_-475207552| |v_~#__CS_thread_status~0.base_2_const_-48473259|) |v_~#__CS_thread_status~0.offset_2_const_1684530067| (select (select |v_#memory_$Pointer$.base_30_const_-475207551| |v_~#__CS_thread_status~0.base_2_const_-48473259|) |v_~#__CS_thread_status~0.offset_2_const_1684530067|)))) (= v_~__CS_thread~0.base_9_const_-308947756 (store v_~__CS_thread~0.base_10_const_-335877310 0 |#funAddr~main_thread.base|)) (= |v_#memory_$Pointer$.base_36_const_-475207537| (store |v_#memory_$Pointer$.base_37_const_-475207538| |v_~#flag2~0.base_5_const_-1586400316| (store .cse7 .cse8 (select (select |v_#memory_$Pointer$.base_36_const_-475207537| |v_~#flag2~0.base_5_const_-1586400316|) .cse8)))) (= |v_#memory_$Pointer$.base_47_const_-475207505| (store |v_#memory_$Pointer$.base_48_const_-475207506| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store .cse9 .cse10 (select .cse11 .cse10)))) (= |v_#memory_$Pointer$.offset_30_const_-436731449| (store |v_#memory_$Pointer$.offset_31_const_-436731450| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store (select |v_#memory_$Pointer$.offset_31_const_-436731450| |v_~#__CS_thread_status~0.base_2_const_-48473259|) |v_~#__CS_thread_status~0.offset_2_const_1684530067| (select (select |v_#memory_$Pointer$.offset_30_const_-436731449| |v_~#__CS_thread_status~0.base_2_const_-48473259|) |v_~#__CS_thread_status~0.offset_2_const_1684530067|)))) (= (store |v_#memory_$Pointer$.offset_49_const_-436731409| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store .cse12 .cse13 (select .cse14 .cse13))) |v_#memory_$Pointer$.offset_48_const_-436731412|) (= |v_#memory_$Pointer$.base_33_const_-475207550| (store |v_#memory_$Pointer$.base_34_const_-475207539| |v_~#x~0.base_6_const_-402024747| (store (select |v_#memory_$Pointer$.base_34_const_-475207539| |v_~#x~0.base_6_const_-402024747|) .cse15 (select .cse16 .cse15)))) (= (store |v_#memory_$Pointer$.offset_35_const_-436731454| |v_~#turn~0.base_6_const_2109769878| (store .cse17 .cse18 (select (select |v_#memory_$Pointer$.offset_34_const_-436731453| |v_~#turn~0.base_6_const_2109769878|) .cse18))) |v_#memory_$Pointer$.offset_34_const_-436731453|) (= |v_#memory_$Pointer$.offset_39_const_-436731442| (let ((.cse19 (store |v_#memory_$Pointer$.offset_46_const_-436731422| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| (let ((.cse22 (let ((.cse25 (let ((.cse28 (let ((.cse31 (let ((.cse33 (store (select |v_#memory_$Pointer$.offset_46_const_-436731422| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646|) .cse35 (select (select |v_#memory_$Pointer$.offset_46_const_-436731422| |v_main_~#__CS_cp___CS_thread_lockedon~0.base_2_const_-1933732893|) .cse36)))) (store .cse33 .cse6 (select (select (store |v_#memory_$Pointer$.offset_46_const_-436731422| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| .cse33) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_2_const_-1933732893|) .cse34))))) (store .cse31 .cse1 (select (select (store |v_#memory_$Pointer$.offset_46_const_-436731422| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| .cse31) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_2_const_-1933732893|) .cse32))))) (store .cse28 .cse29 (select (select (store |v_#memory_$Pointer$.offset_46_const_-436731422| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| .cse28) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_2_const_-1933732893|) .cse30))))) (store .cse25 .cse26 (select (select (store |v_#memory_$Pointer$.offset_46_const_-436731422| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| .cse25) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_2_const_-1933732893|) .cse27))))) (store .cse22 .cse23 (select (select (store |v_#memory_$Pointer$.offset_46_const_-436731422| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| .cse22) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_2_const_-1933732893|) .cse24)))))) (store .cse19 |v_~#flag1~0.base_5_const_-1389894365| (store (select .cse19 |v_~#flag1~0.base_5_const_-1389894365|) .cse20 (select .cse21 .cse20))))) (= |v_#memory_$Pointer$.offset_31_const_-436731450| (store |v_#memory_$Pointer$.offset_32_const_-436731455| |v_~#__CS_thread_born_round~0.base_2_const_1720302587| (store (select |v_#memory_$Pointer$.offset_32_const_-436731455| |v_~#__CS_thread_born_round~0.base_2_const_1720302587|) |v_~#__CS_thread_born_round~0.offset_2_const_544850617| (select (select |v_#memory_$Pointer$.offset_31_const_-436731450| |v_~#__CS_thread_born_round~0.base_2_const_1720302587|) |v_~#__CS_thread_born_round~0.offset_2_const_544850617|)))) (= |v_#memory_$Pointer$.base_31_const_-475207552| (store |v_#memory_$Pointer$.base_32_const_-475207549| |v_~#__CS_thread_born_round~0.base_2_const_1720302587| (store (select |v_#memory_$Pointer$.base_32_const_-475207549| |v_~#__CS_thread_born_round~0.base_2_const_1720302587|) |v_~#__CS_thread_born_round~0.offset_2_const_544850617| (select (select |v_#memory_$Pointer$.base_31_const_-475207552| |v_~#__CS_thread_born_round~0.base_2_const_1720302587|) |v_~#__CS_thread_born_round~0.offset_2_const_544850617|)))) (= (store |v_#memory_$Pointer$.offset_30_const_-436731449| |v_~#__CS_thread_allocated~0.base_2_const_1055191042| (store (select |v_#memory_$Pointer$.offset_30_const_-436731449| |v_~#__CS_thread_allocated~0.base_2_const_1055191042|) |v_~#__CS_thread_allocated~0.offset_2_const_1454422272| (select (select |v_#memory_$Pointer$.offset_29_const_-436731863| |v_~#__CS_thread_allocated~0.base_2_const_1055191042|) |v_~#__CS_thread_allocated~0.offset_2_const_1454422272|))) |v_#memory_$Pointer$.offset_29_const_-436731863|) (= |v_main_#t~mem66_1_const_204362872| (select (select |v_#memory_int_36_const_1545201554| |v_~#__CS_thread_allocated~0.base_2_const_1055191042|) |v_~#__CS_thread_allocated~0.offset_2_const_1454422272|)) (= (store |v_#memory_$Pointer$.base_51_const_-475207610| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store .cse4 .cse37 (select .cse38 .cse37))) |v_#memory_$Pointer$.base_50_const_-475207609|) (= (store |v_#memory_$Pointer$.offset_33_const_-436731456| |v_~#x~0.base_6_const_-402024747| (store .cse39 .cse40 (select (select |v_#memory_$Pointer$.offset_32_const_-436731455| |v_~#x~0.base_6_const_-402024747|) .cse40))) |v_#memory_$Pointer$.offset_32_const_-436731455|) (= v_~__CS_thread_index~0_6_const_-147234545 0) (= |v_#memory_int_47_const_1545201586| (store |v_#memory_int_48_const_1545201597| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| (store .cse41 .cse23 (select (select |v_#memory_int_47_const_1545201586| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646|) .cse23)))) (= (store |v_#memory_$Pointer$.offset_38_const_-436731441| |v_~#flag2~0.base_5_const_-1586400316| (store (select |v_#memory_$Pointer$.offset_38_const_-436731441| |v_~#flag2~0.base_5_const_-1586400316|) .cse42 (select .cse43 .cse42))) |v_#memory_$Pointer$.offset_37_const_-436731444|) (= |v_#memory_$Pointer$.offset_49_const_-436731409| (store |v_#memory_$Pointer$.offset_50_const_-436731515| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store .cse44 .cse45 (select .cse12 .cse45)))) (= (store |v_#memory_$Pointer$.base_36_const_-475207537| |v_~#turn~0.base_6_const_2109769878| (store (select |v_#memory_$Pointer$.base_36_const_-475207537| |v_~#turn~0.base_6_const_2109769878|) .cse46 (select .cse47 .cse46))) |v_#memory_$Pointer$.base_35_const_-475207540|) (= |v_#memory_$Pointer$.offset_33_const_-436731456| (store |v_#memory_$Pointer$.offset_34_const_-436731453| |v_~#x~0.base_6_const_-402024747| (store (select |v_#memory_$Pointer$.offset_34_const_-436731453| |v_~#x~0.base_6_const_-402024747|) .cse15 (select .cse39 .cse15)))) (= |v_#memory_$Pointer$.offset_38_const_-436731441| (store |v_#memory_$Pointer$.offset_39_const_-436731442| |v_~#flag1~0.base_5_const_-1389894365| (store .cse21 .cse48 (select (select |v_#memory_$Pointer$.offset_38_const_-436731441| |v_~#flag1~0.base_5_const_-1389894365|) .cse48)))) (= v_~__CS_round~0_72_const_-563051909 0) (= |v_#memory_$Pointer$.offset_36_const_-436731443| (store |v_#memory_$Pointer$.offset_37_const_-436731444| |v_~#flag2~0.base_5_const_-1586400316| (store .cse43 .cse8 (select (select |v_#memory_$Pointer$.offset_36_const_-436731443| |v_~#flag2~0.base_5_const_-1586400316|) .cse8)))) (= (let ((.cse49 (store |v_#memory_int_59_const_1545201501| |v_~#__CS_thread_status~0.base_2_const_-48473259| (let ((.cse50 (let ((.cse52 (let ((.cse53 (let ((.cse54 (let ((.cse55 (store (select |v_#memory_int_59_const_1545201501| |v_~#__CS_thread_status~0.base_2_const_-48473259|) .cse3 (select (select |v_#memory_int_59_const_1545201501| |v_main_~#__CS_cp___CS_thread_status~0.base_2_const_1635486156|) (+ |v_main_~#__CS_cp___CS_thread_status~0.offset_2_const_649365578| 3))))) (store .cse55 .cse37 (select (select (store |v_#memory_int_59_const_1545201501| |v_~#__CS_thread_status~0.base_2_const_-48473259| .cse55) |v_main_~#__CS_cp___CS_thread_status~0.base_2_const_1635486156|) (+ |v_main_~#__CS_cp___CS_thread_status~0.offset_2_const_649365578| 6)))))) (store .cse54 .cse45 (select (select (store |v_#memory_int_59_const_1545201501| |v_~#__CS_thread_status~0.base_2_const_-48473259| .cse54) |v_main_~#__CS_cp___CS_thread_status~0.base_2_const_1635486156|) (+ |v_main_~#__CS_cp___CS_thread_status~0.offset_2_const_649365578| 4)))))) (store .cse53 .cse13 (select (select (store |v_#memory_int_59_const_1545201501| |v_~#__CS_thread_status~0.base_2_const_-48473259| .cse53) |v_main_~#__CS_cp___CS_thread_status~0.base_2_const_1635486156|) (+ |v_main_~#__CS_cp___CS_thread_status~0.offset_2_const_649365578| 7)))))) (store .cse52 .cse10 (select (select (store |v_#memory_int_59_const_1545201501| |v_~#__CS_thread_status~0.base_2_const_-48473259| .cse52) |v_main_~#__CS_cp___CS_thread_status~0.base_2_const_1635486156|) (+ |v_main_~#__CS_cp___CS_thread_status~0.offset_2_const_649365578| 5)))))) (store .cse50 .cse51 (select (select (store |v_#memory_int_59_const_1545201501| |v_~#__CS_thread_status~0.base_2_const_-48473259| .cse50) |v_main_~#__CS_cp___CS_thread_status~0.base_2_const_1635486156|) (+ |v_main_~#__CS_cp___CS_thread_status~0.offset_2_const_649365578| 8))))))) (store .cse49 |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| (store (select .cse49 |v_~#__CS_thread_lockedon~0.base_4_const_-898830646|) .cse35 (select .cse5 .cse35)))) |v_#memory_int_52_const_1545201492|) (= |v_#memory_$Pointer$.base_46_const_-475207508| (store |v_#memory_$Pointer$.base_47_const_-475207505| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store .cse11 .cse51 (select (select |v_#memory_$Pointer$.base_46_const_-475207508| |v_~#__CS_thread_status~0.base_2_const_-48473259|) .cse51)))) (= (store |v_#memory_$Pointer$.base_50_const_-475207609| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store .cse38 .cse45 (select .cse56 .cse45))) |v_#memory_$Pointer$.base_49_const_-475207511|) (= v_~__CS_thread~0.offset_9_const_-97333358 (store v_~__CS_thread~0.offset_10_const_1266608196 0 |#funAddr~main_thread.offset|)) (= |v_#memory_$Pointer$.offset_35_const_-436731454| (store |v_#memory_$Pointer$.offset_36_const_-436731443| |v_~#turn~0.base_6_const_2109769878| (store (select |v_#memory_$Pointer$.offset_36_const_-436731443| |v_~#turn~0.base_6_const_2109769878|) .cse46 (select .cse17 .cse46)))) (= (store |v_#memory_$Pointer$.offset_51_const_-436731516| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store .cse57 .cse37 (select .cse44 .cse37))) |v_#memory_$Pointer$.offset_50_const_-436731515|) (= |v_#memory_$Pointer$.offset_46_const_-436731422| (store |v_#memory_$Pointer$.offset_47_const_-436731411| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store .cse58 .cse51 (select (select |v_#memory_$Pointer$.offset_46_const_-436731422| |v_~#__CS_thread_status~0.base_2_const_-48473259|) .cse51)))) (= (store |v_#memory_$Pointer$.base_39_const_-475207544| |v_~#flag1~0.base_5_const_-1389894365| (store .cse59 .cse48 (select (select |v_#memory_$Pointer$.base_38_const_-475207543| |v_~#flag1~0.base_5_const_-1389894365|) .cse48))) |v_#memory_$Pointer$.base_38_const_-475207543|) (= (store |v_#memory_$Pointer$.base_38_const_-475207543| |v_~#flag2~0.base_5_const_-1586400316| (store (select |v_#memory_$Pointer$.base_38_const_-475207543| |v_~#flag2~0.base_5_const_-1586400316|) .cse42 (select .cse7 .cse42))) |v_#memory_$Pointer$.base_37_const_-475207538|) (= (store |v_#memory_$Pointer$.base_30_const_-475207551| |v_~#__CS_thread_allocated~0.base_2_const_1055191042| (store (select |v_#memory_$Pointer$.base_30_const_-475207551| |v_~#__CS_thread_allocated~0.base_2_const_1055191042|) |v_~#__CS_thread_allocated~0.offset_2_const_1454422272| (select (select |v_#memory_$Pointer$.base_29_const_-475207445| |v_~#__CS_thread_allocated~0.base_2_const_1055191042|) |v_~#__CS_thread_allocated~0.offset_2_const_1454422272|))) |v_#memory_$Pointer$.base_29_const_-475207445|) (= (store |v_#memory_$Pointer$.base_49_const_-475207511| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store .cse56 .cse13 (select .cse9 .cse13))) |v_#memory_$Pointer$.base_48_const_-475207506|) (= (store |v_#memory_int_49_const_1545201596| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| (store .cse60 .cse26 (select .cse41 .cse26))) |v_#memory_int_48_const_1545201597|) (= (store |v_#memory_$Pointer$.offset_52_const_-436731513| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store (select |v_#memory_$Pointer$.offset_52_const_-436731513| |v_~#__CS_thread_status~0.base_2_const_-48473259|) .cse3 (select .cse57 .cse3))) |v_#memory_$Pointer$.offset_51_const_-436731516|) (= (store |v_#memory_$Pointer$.offset_48_const_-436731412| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store .cse14 .cse10 (select .cse58 .cse10))) |v_#memory_$Pointer$.offset_47_const_-436731411|) (= (store |v_#memory_int_50_const_1545201482| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| (store .cse2 .cse29 (select .cse60 .cse29))) |v_#memory_int_49_const_1545201596|) (= (let ((.cse61 (let ((.cse62 (let ((.cse63 (let ((.cse64 (let ((.cse66 (let ((.cse68 (store |v_#memory_int_47_const_1545201586| |v_~#flag1~0.base_5_const_-1389894365| (let ((.cse70 (store (select |v_#memory_int_47_const_1545201586| |v_~#flag1~0.base_5_const_-1389894365|) .cse20 (select (select |v_#memory_int_47_const_1545201586| |v_main_~#__CS_cp_flag1~0.base_1_const_685083920|) (+ |v_main_~#__CS_cp_flag1~0.offset_1_const_2139279086| 4))))) (store .cse70 .cse48 (select (select (store |v_#memory_int_47_const_1545201586| |v_~#flag1~0.base_5_const_-1389894365| .cse70) |v_main_~#__CS_cp_flag1~0.base_1_const_685083920|) (+ |v_main_~#__CS_cp_flag1~0.offset_1_const_2139279086| 8))))))) (store .cse68 |v_~#flag2~0.base_5_const_-1586400316| (let ((.cse69 (store (select .cse68 |v_~#flag2~0.base_5_const_-1586400316|) .cse42 (select (select .cse68 |v_main_~#__CS_cp_flag2~0.base_1_const_488578097|) (+ |v_main_~#__CS_cp_flag2~0.offset_1_const_-2026608305| 4))))) (store .cse69 .cse8 (select (select (store .cse68 |v_~#flag2~0.base_5_const_-1586400316| .cse69) |v_main_~#__CS_cp_flag2~0.base_1_const_488578097|) (+ |v_main_~#__CS_cp_flag2~0.offset_1_const_-2026608305| 8)))))))) (store .cse66 |v_~#turn~0.base_6_const_2109769878| (let ((.cse67 (store (select .cse66 |v_~#turn~0.base_6_const_2109769878|) .cse46 (select (select .cse66 |v_main_~#__CS_cp_turn~0.base_1_const_-594232398|) (+ |v_main_~#__CS_cp_turn~0.offset_1_const_1195896048| 4))))) (store .cse67 .cse18 (select (select (store .cse66 |v_~#turn~0.base_6_const_2109769878| .cse67) |v_main_~#__CS_cp_turn~0.base_1_const_-594232398|) (+ |v_main_~#__CS_cp_turn~0.offset_1_const_1195896048| 8)))))))) (store .cse64 |v_~#x~0.base_6_const_-402024747| (let ((.cse65 (store (select .cse64 |v_~#x~0.base_6_const_-402024747|) .cse15 (select (select .cse64 |v_main_~#__CS_cp_x~0.base_1_const_-969430205|) (+ |v_main_~#__CS_cp_x~0.offset_1_const_1290085441| 4))))) (store .cse65 .cse40 (select (select (store .cse64 |v_~#x~0.base_6_const_-402024747| .cse65) |v_main_~#__CS_cp_x~0.base_1_const_-969430205|) (+ |v_main_~#__CS_cp_x~0.offset_1_const_1290085441| 8)))))))) (store .cse63 |v_~#__CS_thread_born_round~0.base_2_const_1720302587| (store (select .cse63 |v_~#__CS_thread_born_round~0.base_2_const_1720302587|) |v_~#__CS_thread_born_round~0.offset_2_const_544850617| v_~__CS_round~0_72_const_-563051909))))) (store .cse62 |v_~#__CS_thread_status~0.base_2_const_-48473259| (store (select .cse62 |v_~#__CS_thread_status~0.base_2_const_-48473259|) |v_~#__CS_thread_status~0.offset_2_const_1684530067| v_~__THREAD_RUNNING~0_2_const_278392747))))) (store .cse61 |v_~#__CS_thread_allocated~0.base_2_const_1055191042| (store (select .cse61 |v_~#__CS_thread_allocated~0.base_2_const_1055191042|) |v_~#__CS_thread_allocated~0.offset_2_const_1454422272| 1))) |v_#memory_int_36_const_1545201554|) (= |v_#memory_$Pointer$.base_34_const_-475207539| (store |v_#memory_$Pointer$.base_35_const_-475207540| |v_~#turn~0.base_6_const_2109769878| (store .cse47 .cse18 (select (select |v_#memory_$Pointer$.base_34_const_-475207539| |v_~#turn~0.base_6_const_2109769878|) .cse18)))) (= (store |v_#memory_$Pointer$.base_33_const_-475207550| |v_~#x~0.base_6_const_-402024747| (store .cse16 .cse40 (select (select |v_#memory_$Pointer$.base_32_const_-475207549| |v_~#x~0.base_6_const_-402024747|) .cse40))) |v_#memory_$Pointer$.base_32_const_-475207549|) (= (let ((.cse71 (store |v_#memory_$Pointer$.base_46_const_-475207508| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| (let ((.cse72 (let ((.cse73 (let ((.cse74 (let ((.cse75 (let ((.cse76 (store (select |v_#memory_$Pointer$.base_46_const_-475207508| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646|) .cse35 (select (select |v_#memory_$Pointer$.base_46_const_-475207508| |v_main_~#__CS_cp___CS_thread_lockedon~0.base_2_const_-1933732893|) .cse36)))) (store .cse76 .cse6 (select (select (store |v_#memory_$Pointer$.base_46_const_-475207508| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| .cse76) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_2_const_-1933732893|) .cse34))))) (store .cse75 .cse1 (select (select (store |v_#memory_$Pointer$.base_46_const_-475207508| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| .cse75) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_2_const_-1933732893|) .cse32))))) (store .cse74 .cse29 (select (select (store |v_#memory_$Pointer$.base_46_const_-475207508| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| .cse74) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_2_const_-1933732893|) .cse30))))) (store .cse73 .cse26 (select (select (store |v_#memory_$Pointer$.base_46_const_-475207508| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| .cse73) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_2_const_-1933732893|) .cse27))))) (store .cse72 .cse23 (select (select (store |v_#memory_$Pointer$.base_46_const_-475207508| |v_~#__CS_thread_lockedon~0.base_4_const_-898830646| .cse72) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_2_const_-1933732893|) .cse24)))))) (store .cse71 |v_~#flag1~0.base_5_const_-1389894365| (store (select .cse71 |v_~#flag1~0.base_5_const_-1389894365|) .cse20 (select .cse59 .cse20)))) |v_#memory_$Pointer$.base_39_const_-475207544|))))
(check-sat)
(exit)