blob: d36f62b16e94fe93e4da8b0ae3a536a959fc42db (
plain)
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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
|
; COMMAND-LINE: --incremental
; EXPECT: sat
; EXPECT: sat
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(declare-fun |__ADDRESS_OF_main::c1| () Real)
(declare-fun |__ADDRESS_OF_main::x1| () Real)
(declare-fun |__ADDRESS_OF_main::x2| () Real)
(declare-fun |__ADDRESS_OF_main::c2| () Real)
(declare-fun |main::x3@3| () Real)
(declare-fun |main::x1@3| () Real)
(declare-fun |__ADDRESS_OF_main::d3| () Real)
(declare-fun __BASE_ADDRESS_OF__ (Real) Real)
(declare-fun |main::x2@3| () Real)
(declare-fun |main::d3@2| () Real)
(declare-fun |__VERIFIER_assert::cond@2| () Real)
(declare-fun |__ADDRESS_OF_main::x3| () Real)
(declare-fun |main::d1@2| () Real)
(declare-fun |__ADDRESS_OF_main::d2| () Real)
(declare-fun |__ADDRESS_OF_main::__CPAchecker_TMP_0| () Real)
(declare-fun |main::__CPAchecker_TMP_0@3| () Real)
(declare-fun |__ADDRESS_OF_main::d1| () Real)
(declare-fun |main::d2@2| () Real)
(define-fun _7 () Real 0)
(define-fun _8 () Real |__ADDRESS_OF_main::x1|)
(define-fun _9 () Real (__BASE_ADDRESS_OF__ _8))
(define-fun _10 () Bool (= _8 _9))
(define-fun _11 () Real |__ADDRESS_OF_main::x2|)
(define-fun _12 () Real (__BASE_ADDRESS_OF__ _11))
(define-fun _13 () Bool (= _11 _12))
(define-fun _14 () Bool (and _10 _13))
(define-fun _15 () Real |__ADDRESS_OF_main::x3|)
(define-fun _16 () Real (__BASE_ADDRESS_OF__ _15))
(define-fun _17 () Bool (= _15 _16))
(define-fun _18 () Bool (and _14 _17))
(define-fun _19 () Real |__ADDRESS_OF_main::d1|)
(define-fun _20 () Real (__BASE_ADDRESS_OF__ _19))
(define-fun _21 () Bool (= _19 _20))
(define-fun _22 () Real 1)
(define-fun _23 () Real |main::d1@2|)
(define-fun _24 () Bool (= _23 _22))
(define-fun _25 () Bool (and _21 _24))
(define-fun _26 () Bool (and _18 _25))
(define-fun _27 () Real |__ADDRESS_OF_main::d2|)
(define-fun _28 () Real (__BASE_ADDRESS_OF__ _27))
(define-fun _29 () Bool (= _27 _28))
(define-fun _30 () Real |main::d2@2|)
(define-fun _31 () Bool (= _30 _22))
(define-fun _32 () Bool (and _29 _31))
(define-fun _33 () Bool (and _26 _32))
(define-fun _34 () Real |__ADDRESS_OF_main::d3|)
(define-fun _35 () Real (__BASE_ADDRESS_OF__ _34))
(define-fun _36 () Bool (= _34 _35))
(define-fun _37 () Real |main::d3@2|)
(define-fun _38 () Bool (= _37 _22))
(define-fun _39 () Bool (and _36 _38))
(define-fun _40 () Bool (and _33 _39))
(define-fun _41 () Real |__ADDRESS_OF_main::c1|)
(define-fun _42 () Real (__BASE_ADDRESS_OF__ _41))
(define-fun _43 () Bool (= _41 _42))
(define-fun _44 () Bool (and _40 _43))
(define-fun _45 () Real |__ADDRESS_OF_main::c2|)
(define-fun _46 () Real (__BASE_ADDRESS_OF__ _45))
(define-fun _47 () Bool (= _45 _46))
(define-fun _48 () Bool (and _44 _47))
(define-fun _49 () Real |main::x1@3|)
(define-fun _50 () Bool (<= _49 _7))
(define-fun _51 () Bool (not _50))
(define-fun _53 () Bool (and _48 _51))
(define-fun _54 () Bool (and _48 _50))
(define-fun _55 () Real |main::x2@3|)
(define-fun _56 () Bool (<= _55 _7))
(define-fun _57 () Bool (not _56))
(define-fun _59 () Bool (and _53 _57))
(define-fun _60 () Bool (and _53 _56))
(define-fun _61 () Bool (or _54 _60))
(define-fun _62 () Real |main::x3@3|)
(define-fun _63 () Bool (<= _62 _7))
(define-fun _67 () Bool (and _59 _63))
(define-fun _68 () Bool (or _61 _67))
(define-fun _69 () Real |__ADDRESS_OF_main::__CPAchecker_TMP_0|)
(define-fun _70 () Real (__BASE_ADDRESS_OF__ _69))
(define-fun _71 () Bool (= _69 _70))
(define-fun _72 () Bool (and _68 _71))
(define-fun _73 () Bool (= _49 _7))
(define-fun _75 () Bool (and _72 _73))
(define-fun _76 () Bool (not _73))
(define-fun _77 () Bool (and _72 _76))
(define-fun _78 () Bool (= _55 _7))
(define-fun _80 () Bool (and _77 _78))
(define-fun _81 () Bool (not _78))
(define-fun _82 () Bool (and _77 _81))
(define-fun _83 () Bool (or _75 _80))
(define-fun _84 () Bool (= _62 _7))
(define-fun _86 () Bool (and _82 _84))
(define-fun _87 () Bool (not _84))
(define-fun _88 () Bool (and _82 _87))
(define-fun _89 () Bool (or _83 _86))
(define-fun _90 () Real |main::__CPAchecker_TMP_0@3|)
(define-fun _91 () Bool (= _90 _7))
(define-fun _92 () Bool (and _88 _91))
(define-fun _93 () Bool (= _90 _22))
(define-fun _94 () Bool (and _89 _93))
(define-fun _95 () Bool (or _92 _94))
(define-fun _96 () Real |__VERIFIER_assert::cond@2|)
(define-fun _97 () Bool (= _90 _96))
(define-fun _98 () Bool (and _95 _97))
(define-fun _99 () Bool (= _96 _7))
(define-fun _101 () Bool (and _98 _99))
(declare-fun __ART__34@0 () Bool)
(declare-fun |main::c2@3| () Real)
(declare-fun __ART__24@0 () Bool)
(declare-fun __ART__45@0 () Bool)
(declare-fun |main::c1@3| () Real)
(declare-fun __ART__23@0 () Bool)
(declare-fun __ART__32@0 () Bool)
(declare-fun __ART__36@0 () Bool)
(declare-fun __ART__26@0 () Bool)
(declare-fun __ART__53@0 () Bool)
(declare-fun __ART__29@0 () Bool)
(define-fun _64 () Bool (not _63))
(define-fun _108 () Real |main::c1@3|)
(define-fun _109 () Bool (= _108 _7))
(define-fun _123 () Real |main::c2@3|)
(define-fun _124 () Bool (= _123 _7))
(define-fun _160 () Bool __ART__23@0)
(define-fun _161 () Bool (= _51 _160))
(define-fun _162 () Bool __ART__24@0)
(define-fun _163 () Bool (= _57 _162))
(define-fun _164 () Bool (and _161 _163))
(define-fun _165 () Bool __ART__26@0)
(define-fun _166 () Bool (= _64 _165))
(define-fun _167 () Bool (and _164 _166))
(define-fun _168 () Bool __ART__29@0)
(define-fun _169 () Bool (= _109 _168))
(define-fun _170 () Bool (and _167 _169))
(define-fun _171 () Bool __ART__32@0)
(define-fun _172 () Bool (= _73 _171))
(define-fun _173 () Bool (and _170 _172))
(define-fun _174 () Bool __ART__34@0)
(define-fun _175 () Bool (= _78 _174))
(define-fun _176 () Bool (and _173 _175))
(define-fun _177 () Bool __ART__36@0)
(define-fun _178 () Bool (= _84 _177))
(define-fun _179 () Bool (and _176 _178))
(define-fun _180 () Bool __ART__45@0)
(define-fun _181 () Bool (= _99 _180))
(define-fun _182 () Bool (and _179 _181))
(define-fun _183 () Bool __ART__53@0)
(define-fun _184 () Bool (= _124 _183))
(define-fun _185 () Bool (and _182 _184))
(push 1)
(assert _101)
(set-info :status sat)
(check-sat)
(push 1)
(assert _185)
(set-info :status sat)
(check-sat)
(pop 1)
(pop 1)
(exit)
|
