cs_sync_true-unreach-call.i_0.smt2 21.9 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
(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 sat)
(declare-fun |#funAddr~thread1.base| () Int)
(declare-fun |#funAddr~thread1.offset| () Int)
(declare-fun |#funAddr~thread2.base| () Int)
(declare-fun |#funAddr~thread2.offset| () Int)
(declare-fun |#funAddr~main_thread.base| () Int)
(declare-fun |#funAddr~main_thread.offset| () Int)
(declare-fun ~__codecvt_result~0~__codecvt_ok () Int)
(declare-fun ~__codecvt_result~0~__codecvt_partial () Int)
(declare-fun ~__codecvt_result~0~__codecvt_error () Int)
(declare-fun ~__codecvt_result~0~__codecvt_noconv () 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~thread1.offset|) (= |#funAddr~thread1.base| (- 1))))
(assert (and (= |#funAddr~thread2.offset| 1) (= |#funAddr~thread2.base| (- 1))))
(assert (and (= 2 |#funAddr~main_thread.offset|) (= |#funAddr~main_thread.base| (- 1))))
(assert (= ~__codecvt_result~0~__codecvt_ok 0))
(assert (= 1 ~__codecvt_result~0~__codecvt_partial))
(assert (= 2 ~__codecvt_result~0~__codecvt_error))
(assert (= ~__codecvt_result~0~__codecvt_noconv 3))
(assert (= ~unnamed0~0~P_ALL 0))
(assert (= ~unnamed0~0~P_PID 1))
(assert (= 2 ~unnamed0~0~P_PGID))
(declare-fun |v_#memory_int_51_const_1545201493| () (Array Int (Array Int Int)))
(declare-fun |v_main_~#__CS_cp_num~0.base_1_const_607855665| () Int)
(declare-fun |v_main_~#__CS_cp_num~0.offset_1_const_941797711| () Int)
(declare-fun |v_~#num~0.base_8_const_417860993| () Int)
(declare-fun |v_~#num~0.offset_8_const_-1133049505| () Int)
(declare-fun |v_main_~#__CS_cp_m~0.base_1_const_1192216568| () Int)
(declare-fun |v_main_~#__CS_cp_m~0.offset_1_const_-129810506| () Int)
(declare-fun |v_~#m~0.base_9_const_1759621895| () Int)
(declare-fun |v_~#m~0.offset_9_const_-319690491| () Int)
(declare-fun |v_main_~#__CS_cp_empty~0.base_1_const_-316245224| () Int)
(declare-fun |v_main_~#__CS_cp_empty~0.offset_1_const_2053839574| () Int)
(declare-fun |v_~#empty~0.base_5_const_1903743787| () Int)
(declare-fun |v_~#empty~0.offset_5_const_868454697| () Int)
(declare-fun |v_main_~#__CS_cp_full~0.base_1_const_1803364708| () Int)
(declare-fun |v_main_~#__CS_cp_full~0.offset_1_const_-1227837918| () Int)
(declare-fun |v_~#full~0.base_5_const_212416073| () Int)
(declare-fun |v_~#full~0.offset_5_const_-1127394105| () 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_75_const_-563051912 () 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_44_const_1545201585| () (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_40_const_-475207514| () (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_main_#t~mem95_1_const_204585692| () Int)
(declare-fun |v_#memory_$Pointer$.offset_38_const_-436731441| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_39_const_-436731442| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_50_const_-475207609| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_51_const_-475207610| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_50_const_-436731515| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_51_const_-436731516| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_41_const_-475207519| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_43_const_-475207517| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_44_const_-475207518| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_43_const_-436731423| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_44_const_-436731424| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_42_const_-475207520| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_41_const_-436731417| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_42_const_-436731418| () (Array Int (Array Int Int)))
(declare-fun |v_~#__CS_thread_lockedon~0.base_6_const_-898830648| () Int)
(declare-fun |v_~#__CS_thread_lockedon~0.offset_6_const_541011270| () Int)
(declare-fun |v_#memory_int_52_const_1545201492| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_49_const_-436731409| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_48_const_-436731412| () (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_~__CS_thread_index~0_9_const_-147234548 () Int)
(declare-fun |v_#memory_$Pointer$.offset_40_const_-436731420| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_38_const_-475207543| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_53_const_1545201495| () (Array Int (Array Int Int)))
(declare-fun |v_main_~#__CS_cp___CS_thread_lockedon~0.base_1_const_-1933732892| () Int)
(declare-fun |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_1_const_-1991001950| () Int)
(declare-fun |v_#memory_$Pointer$.base_48_const_-475207506| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_57_const_1545201491| () (Array Int (Array Int Int)))
(declare-fun |v_main_~#__CS_cp___CS_thread_status~0.base_1_const_1635486157| () Int)
(declare-fun |v_main_~#__CS_cp___CS_thread_status~0.offset_1_const_649365579| () Int)
(assert (let ((.cse3 (+ |v_~#m~0.offset_9_const_-319690491| 1)) (.cse5 (+ |v_~#full~0.offset_5_const_-1127394105| 1)) (.cse4 (+ |v_~#empty~0.offset_5_const_868454697| 1)) (.cse2 (select |v_#memory_$Pointer$.offset_50_const_-436731515| |v_~#__CS_thread_status~0.base_2_const_-48473259|)) (.cse16 (select |v_#memory_$Pointer$.offset_49_const_-436731409| |v_~#__CS_thread_status~0.base_2_const_-48473259|)) (.cse1 (select |v_#memory_$Pointer$.base_50_const_-475207609| |v_~#__CS_thread_status~0.base_2_const_-48473259|)) (.cse6 (select |v_#memory_int_52_const_1545201492| |v_~#__CS_thread_lockedon~0.base_6_const_-898830648|)) (.cse14 (+ |v_~#num~0.offset_8_const_-1133049505| 4)) (.cse7 (+ |v_~#__CS_thread_lockedon~0.offset_6_const_541011270| 40)) (.cse23 (+ |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_1_const_-1991001950| 40)) (.cse20 (+ |v_~#__CS_thread_lockedon~0.offset_6_const_541011270| 32)) (.cse25 (+ |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_1_const_-1991001950| 32)) (.cse27 (+ |v_main_~#__CS_cp___CS_thread_lockedon~0.offset_1_const_-1991001950| 24)) (.cse19 (select |v_#memory_int_53_const_1545201495| |v_~#__CS_thread_lockedon~0.base_6_const_-898830648|)) (.cse26 (+ |v_~#__CS_thread_lockedon~0.offset_6_const_541011270| 24)) (.cse15 (+ |v_~#__CS_thread_status~0.offset_2_const_1684530067| 4)) (.cse0 (+ |v_~#__CS_thread_status~0.offset_2_const_1684530067| 3)) (.cse18 (select |v_#memory_$Pointer$.base_49_const_-475207511| |v_~#__CS_thread_status~0.base_2_const_-48473259|)) (.cse17 (+ |v_~#__CS_thread_status~0.offset_2_const_1684530067| 5))) (and (= |v_#memory_$Pointer$.base_39_const_-475207544| (store |v_#memory_$Pointer$.base_40_const_-475207514| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store (select |v_#memory_$Pointer$.base_40_const_-475207514| |v_~#__CS_thread_status~0.base_2_const_-48473259|) |v_~#__CS_thread_status~0.offset_2_const_1684530067| (select (select |v_#memory_$Pointer$.base_39_const_-475207544| |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|)) (= (select (select |v_#memory_int_44_const_1545201585| |v_~#__CS_thread_allocated~0.base_2_const_1055191042|) |v_~#__CS_thread_allocated~0.offset_2_const_1454422272|) |v_main_#t~mem95_1_const_204585692|) (= (store |v_#memory_$Pointer$.offset_39_const_-436731442| |v_~#__CS_thread_allocated~0.base_2_const_1055191042| (store (select |v_#memory_$Pointer$.offset_39_const_-436731442| |v_~#__CS_thread_allocated~0.base_2_const_1055191042|) |v_~#__CS_thread_allocated~0.offset_2_const_1454422272| (select (select |v_#memory_$Pointer$.offset_38_const_-436731441| |v_~#__CS_thread_allocated~0.base_2_const_1055191042|) |v_~#__CS_thread_allocated~0.offset_2_const_1454422272|))) |v_#memory_$Pointer$.offset_38_const_-436731441|) (= |v_#memory_$Pointer$.base_50_const_-475207609| (store |v_#memory_$Pointer$.base_51_const_-475207610| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store (select |v_#memory_$Pointer$.base_51_const_-475207610| |v_~#__CS_thread_status~0.base_2_const_-48473259|) .cse0 (select .cse1 .cse0)))) (= |v_#memory_$Pointer$.offset_50_const_-436731515| (store |v_#memory_$Pointer$.offset_51_const_-436731516| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store (select |v_#memory_$Pointer$.offset_51_const_-436731516| |v_~#__CS_thread_status~0.base_2_const_-48473259|) .cse0 (select .cse2 .cse0)))) (= (store |v_#memory_$Pointer$.base_41_const_-475207519| |v_~#__CS_thread_born_round~0.base_2_const_1720302587| (store (select |v_#memory_$Pointer$.base_41_const_-475207519| |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_40_const_-475207514| |v_~#__CS_thread_born_round~0.base_2_const_1720302587|) |v_~#__CS_thread_born_round~0.offset_2_const_544850617|))) |v_#memory_$Pointer$.base_40_const_-475207514|) (= |v_#memory_$Pointer$.base_43_const_-475207517| (store |v_#memory_$Pointer$.base_44_const_-475207518| |v_~#m~0.base_9_const_1759621895| (store (select |v_#memory_$Pointer$.base_44_const_-475207518| |v_~#m~0.base_9_const_1759621895|) .cse3 (select (select |v_#memory_$Pointer$.base_43_const_-475207517| |v_~#m~0.base_9_const_1759621895|) .cse3)))) (= |v_#memory_$Pointer$.offset_43_const_-436731423| (store |v_#memory_$Pointer$.offset_44_const_-436731424| |v_~#m~0.base_9_const_1759621895| (store (select |v_#memory_$Pointer$.offset_44_const_-436731424| |v_~#m~0.base_9_const_1759621895|) .cse3 (select (select |v_#memory_$Pointer$.offset_43_const_-436731423| |v_~#m~0.base_9_const_1759621895|) .cse3)))) (= v_~__CS_round~0_75_const_-563051912 0) (= (store |v_#memory_$Pointer$.base_43_const_-475207517| |v_~#empty~0.base_5_const_1903743787| (store (select |v_#memory_$Pointer$.base_43_const_-475207517| |v_~#empty~0.base_5_const_1903743787|) .cse4 (select (select |v_#memory_$Pointer$.base_42_const_-475207520| |v_~#empty~0.base_5_const_1903743787|) .cse4))) |v_#memory_$Pointer$.base_42_const_-475207520|) (= |v_#memory_$Pointer$.offset_41_const_-436731417| (store |v_#memory_$Pointer$.offset_42_const_-436731418| |v_~#full~0.base_5_const_212416073| (store (select |v_#memory_$Pointer$.offset_42_const_-436731418| |v_~#full~0.base_5_const_212416073|) .cse5 (select (select |v_#memory_$Pointer$.offset_41_const_-436731417| |v_~#full~0.base_5_const_212416073|) .cse5)))) (= (store |v_#memory_int_52_const_1545201492| |v_~#__CS_thread_lockedon~0.base_6_const_-898830648| (store .cse6 .cse7 (select (select |v_#memory_int_51_const_1545201493| |v_~#__CS_thread_lockedon~0.base_6_const_-898830648|) .cse7))) |v_#memory_int_51_const_1545201493|) (= (let ((.cse8 (let ((.cse9 (let ((.cse10 (let ((.cse11 (let ((.cse12 (let ((.cse13 (store |v_#memory_int_51_const_1545201493| |v_~#num~0.base_8_const_417860993| (store (select |v_#memory_int_51_const_1545201493| |v_~#num~0.base_8_const_417860993|) .cse14 (select (select |v_#memory_int_51_const_1545201493| |v_main_~#__CS_cp_num~0.base_1_const_607855665|) (+ |v_main_~#__CS_cp_num~0.offset_1_const_941797711| 4)))))) (store .cse13 |v_~#m~0.base_9_const_1759621895| (store (select .cse13 |v_~#m~0.base_9_const_1759621895|) .cse3 (select (select .cse13 |v_main_~#__CS_cp_m~0.base_1_const_1192216568|) (+ |v_main_~#__CS_cp_m~0.offset_1_const_-129810506| 1))))))) (store .cse12 |v_~#empty~0.base_5_const_1903743787| (store (select .cse12 |v_~#empty~0.base_5_const_1903743787|) .cse4 (select (select .cse12 |v_main_~#__CS_cp_empty~0.base_1_const_-316245224|) (+ |v_main_~#__CS_cp_empty~0.offset_1_const_2053839574| 1))))))) (store .cse11 |v_~#full~0.base_5_const_212416073| (store (select .cse11 |v_~#full~0.base_5_const_212416073|) .cse5 (select (select .cse11 |v_main_~#__CS_cp_full~0.base_1_const_1803364708|) (+ |v_main_~#__CS_cp_full~0.offset_1_const_-1227837918| 1))))))) (store .cse10 |v_~#__CS_thread_born_round~0.base_2_const_1720302587| (store (select .cse10 |v_~#__CS_thread_born_round~0.base_2_const_1720302587|) |v_~#__CS_thread_born_round~0.offset_2_const_544850617| v_~__CS_round~0_75_const_-563051912))))) (store .cse9 |v_~#__CS_thread_status~0.base_2_const_-48473259| (store (select .cse9 |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 .cse8 |v_~#__CS_thread_allocated~0.base_2_const_1055191042| (store (select .cse8 |v_~#__CS_thread_allocated~0.base_2_const_1055191042|) |v_~#__CS_thread_allocated~0.offset_2_const_1454422272| 1))) |v_#memory_int_44_const_1545201585|) (= (store |v_#memory_$Pointer$.base_42_const_-475207520| |v_~#full~0.base_5_const_212416073| (store (select |v_#memory_$Pointer$.base_42_const_-475207520| |v_~#full~0.base_5_const_212416073|) .cse5 (select (select |v_#memory_$Pointer$.base_41_const_-475207519| |v_~#full~0.base_5_const_212416073|) .cse5))) |v_#memory_$Pointer$.base_41_const_-475207519|) (= (store |v_#memory_$Pointer$.offset_43_const_-436731423| |v_~#empty~0.base_5_const_1903743787| (store (select |v_#memory_$Pointer$.offset_43_const_-436731423| |v_~#empty~0.base_5_const_1903743787|) .cse4 (select (select |v_#memory_$Pointer$.offset_42_const_-436731418| |v_~#empty~0.base_5_const_1903743787|) .cse4))) |v_#memory_$Pointer$.offset_42_const_-436731418|) (= |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 .cse2 .cse15 (select .cse16 .cse15)))) (= (store |v_#memory_$Pointer$.offset_49_const_-436731409| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store .cse16 .cse17 (select (select |v_#memory_$Pointer$.offset_48_const_-436731412| |v_~#__CS_thread_status~0.base_2_const_-48473259|) .cse17))) |v_#memory_$Pointer$.offset_48_const_-436731412|) (= (store |v_#memory_$Pointer$.base_50_const_-475207609| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store .cse1 .cse15 (select .cse18 .cse15))) |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_~__CS_thread_index~0_9_const_-147234548 0) (= |v_#memory_$Pointer$.offset_40_const_-436731420| (store |v_#memory_$Pointer$.offset_41_const_-436731417| |v_~#__CS_thread_born_round~0.base_2_const_1720302587| (store (select |v_#memory_$Pointer$.offset_41_const_-436731417| |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_40_const_-436731420| |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_40_const_-436731420| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store (select |v_#memory_$Pointer$.offset_40_const_-436731420| |v_~#__CS_thread_status~0.base_2_const_-48473259|) |v_~#__CS_thread_status~0.offset_2_const_1684530067| (select (select |v_#memory_$Pointer$.offset_39_const_-436731442| |v_~#__CS_thread_status~0.base_2_const_-48473259|) |v_~#__CS_thread_status~0.offset_2_const_1684530067|))) |v_#memory_$Pointer$.offset_39_const_-436731442|) (= |v_#memory_$Pointer$.base_38_const_-475207543| (store |v_#memory_$Pointer$.base_39_const_-475207544| |v_~#__CS_thread_allocated~0.base_2_const_1055191042| (store (select |v_#memory_$Pointer$.base_39_const_-475207544| |v_~#__CS_thread_allocated~0.base_2_const_1055191042|) |v_~#__CS_thread_allocated~0.offset_2_const_1454422272| (select (select |v_#memory_$Pointer$.base_38_const_-475207543| |v_~#__CS_thread_allocated~0.base_2_const_1055191042|) |v_~#__CS_thread_allocated~0.offset_2_const_1454422272|)))) (= |v_#memory_int_52_const_1545201492| (store |v_#memory_int_53_const_1545201495| |v_~#__CS_thread_lockedon~0.base_6_const_-898830648| (store .cse19 .cse20 (select .cse6 .cse20)))) (= (let ((.cse21 (store |v_#memory_$Pointer$.offset_48_const_-436731412| |v_~#__CS_thread_lockedon~0.base_6_const_-898830648| (let ((.cse22 (let ((.cse24 (store (select |v_#memory_$Pointer$.offset_48_const_-436731412| |v_~#__CS_thread_lockedon~0.base_6_const_-898830648|) .cse26 (select (select |v_#memory_$Pointer$.offset_48_const_-436731412| |v_main_~#__CS_cp___CS_thread_lockedon~0.base_1_const_-1933732892|) .cse27)))) (store .cse24 .cse20 (select (select (store |v_#memory_$Pointer$.offset_48_const_-436731412| |v_~#__CS_thread_lockedon~0.base_6_const_-898830648| .cse24) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_1_const_-1933732892|) .cse25))))) (store .cse22 .cse7 (select (select (store |v_#memory_$Pointer$.offset_48_const_-436731412| |v_~#__CS_thread_lockedon~0.base_6_const_-898830648| .cse22) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_1_const_-1933732892|) .cse23)))))) (store .cse21 |v_~#num~0.base_8_const_417860993| (store (select .cse21 |v_~#num~0.base_8_const_417860993|) .cse14 (select (select |v_#memory_$Pointer$.offset_44_const_-436731424| |v_~#num~0.base_8_const_417860993|) .cse14)))) |v_#memory_$Pointer$.offset_44_const_-436731424|) (= (let ((.cse28 (store |v_#memory_$Pointer$.base_48_const_-475207506| |v_~#__CS_thread_lockedon~0.base_6_const_-898830648| (let ((.cse29 (let ((.cse30 (store (select |v_#memory_$Pointer$.base_48_const_-475207506| |v_~#__CS_thread_lockedon~0.base_6_const_-898830648|) .cse26 (select (select |v_#memory_$Pointer$.base_48_const_-475207506| |v_main_~#__CS_cp___CS_thread_lockedon~0.base_1_const_-1933732892|) .cse27)))) (store .cse30 .cse20 (select (select (store |v_#memory_$Pointer$.base_48_const_-475207506| |v_~#__CS_thread_lockedon~0.base_6_const_-898830648| .cse30) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_1_const_-1933732892|) .cse25))))) (store .cse29 .cse7 (select (select (store |v_#memory_$Pointer$.base_48_const_-475207506| |v_~#__CS_thread_lockedon~0.base_6_const_-898830648| .cse29) |v_main_~#__CS_cp___CS_thread_lockedon~0.base_1_const_-1933732892|) .cse23)))))) (store .cse28 |v_~#num~0.base_8_const_417860993| (store (select .cse28 |v_~#num~0.base_8_const_417860993|) .cse14 (select (select |v_#memory_$Pointer$.base_44_const_-475207518| |v_~#num~0.base_8_const_417860993|) .cse14)))) |v_#memory_$Pointer$.base_44_const_-475207518|) (= (let ((.cse31 (store |v_#memory_int_57_const_1545201491| |v_~#__CS_thread_status~0.base_2_const_-48473259| (let ((.cse32 (let ((.cse33 (store (select |v_#memory_int_57_const_1545201491| |v_~#__CS_thread_status~0.base_2_const_-48473259|) .cse0 (select (select |v_#memory_int_57_const_1545201491| |v_main_~#__CS_cp___CS_thread_status~0.base_1_const_1635486157|) (+ |v_main_~#__CS_cp___CS_thread_status~0.offset_1_const_649365579| 3))))) (store .cse33 .cse15 (select (select (store |v_#memory_int_57_const_1545201491| |v_~#__CS_thread_status~0.base_2_const_-48473259| .cse33) |v_main_~#__CS_cp___CS_thread_status~0.base_1_const_1635486157|) (+ |v_main_~#__CS_cp___CS_thread_status~0.offset_1_const_649365579| 4)))))) (store .cse32 .cse17 (select (select (store |v_#memory_int_57_const_1545201491| |v_~#__CS_thread_status~0.base_2_const_-48473259| .cse32) |v_main_~#__CS_cp___CS_thread_status~0.base_1_const_1635486157|) (+ |v_main_~#__CS_cp___CS_thread_status~0.offset_1_const_649365579| 5))))))) (store .cse31 |v_~#__CS_thread_lockedon~0.base_6_const_-898830648| (store (select .cse31 |v_~#__CS_thread_lockedon~0.base_6_const_-898830648|) .cse26 (select .cse19 .cse26)))) |v_#memory_int_53_const_1545201495|) (= |v_#memory_$Pointer$.base_48_const_-475207506| (store |v_#memory_$Pointer$.base_49_const_-475207511| |v_~#__CS_thread_status~0.base_2_const_-48473259| (store .cse18 .cse17 (select (select |v_#memory_$Pointer$.base_48_const_-475207506| |v_~#__CS_thread_status~0.base_2_const_-48473259|) .cse17)))))))
(check-sat)
(exit)