Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_relop_test / relop_test.smt2 @ 6c3ea955

History | View | Annotate | Download (12 KB)

1
; relop_test
2
(declare-var relop_test.In1_1_1 Real)
3
(declare-var relop_test.In2_1_1 Real)
4
(declare-var relop_test.In3_1_1 Int)
5
(declare-var relop_test.In4_1_1 Int)
6
(declare-var relop_test.In5_1_1 Bool)
7
(declare-var relop_test.In6_1_1 Real)
8
(declare-var relop_test.In7_1_1 Real)
9
(declare-var relop_test.In8_1_1 Real)
10
(declare-var relop_test.In9_1_1 Int)
11
(declare-var relop_test.In10_1_1 Int)
12
(declare-var relop_test.In11_1_1 Bool)
13
(declare-var relop_test.In12_1_1 Bool)
14
(declare-var relop_test.In13_1_1 Real)
15
(declare-var relop_test.In14_1_1 Real)
16
(declare-var relop_test.In15_1_1 Int)
17
(declare-var relop_test.In16_1_1 Int)
18
(declare-var relop_test.In17_1_1 Bool)
19
(declare-var relop_test.In18_1_1 Bool)
20
(declare-var relop_test.In19_1_1 Real)
21
(declare-var relop_test.In20_1_1 Real)
22
(declare-var relop_test.In21_1_1 Int)
23
(declare-var relop_test.In22_1_1 Int)
24
(declare-var relop_test.In23_1_1 Bool)
25
(declare-var relop_test.In24_1_1 Bool)
26
(declare-var relop_test.In25_1_1 Real)
27
(declare-var relop_test.In26_1_1 Real)
28
(declare-var relop_test.In27_1_1 Int)
29
(declare-var relop_test.In28_1_1 Int)
30
(declare-var relop_test.In29_1_1 Bool)
31
(declare-var relop_test.In30_1_1 Bool)
32
(declare-var relop_test.In31_1_1 Real)
33
(declare-var relop_test.In32_1_1 Real)
34
(declare-var relop_test.In33_1_1 Int)
35
(declare-var relop_test.In34_1_1 Int)
36
(declare-var relop_test.In35_1_1 Bool)
37
(declare-var relop_test.In36_1_1 Bool)
38
(declare-var relop_test.Out1_1_1 Bool)
39
(declare-var relop_test.Out2_2_1 Bool)
40
(declare-var relop_test.Out3_3_1 Bool)
41
(declare-var relop_test.Out4_4_1 Bool)
42
(declare-var relop_test.Out5_5_1 Bool)
43
(declare-var relop_test.Out6_6_1 Bool)
44
(declare-var relop_test.Out7_7_1 Bool)
45
(declare-var relop_test.Out8_8_1 Bool)
46
(declare-var relop_test.Out9_9_1 Bool)
47
(declare-var relop_test.Out10_10_1 Bool)
48
(declare-var relop_test.Out11_11_1 Bool)
49
(declare-var relop_test.Out12_12_1 Bool)
50
(declare-var relop_test.Out13_13_1 Bool)
51
(declare-var relop_test.Out14_14_1 Bool)
52
(declare-var relop_test.Out15_15_1 Bool)
53
(declare-var relop_test.Out16_16_1 Bool)
54
(declare-var relop_test.Out17_17_1 Bool)
55
(declare-var relop_test.Out18_18_1 Bool)
56
(declare-var relop_test.ni_0._arrow._first_c Bool)
57
(declare-var relop_test.ni_0._arrow._first_m Bool)
58
(declare-var relop_test.ni_0._arrow._first_x Bool)
59
(declare-var relop_test.RelationalOperator10_1_1 Bool)
60
(declare-var relop_test.RelationalOperator11_1_1 Bool)
61
(declare-var relop_test.RelationalOperator12_1_1 Bool)
62
(declare-var relop_test.RelationalOperator13_1_1 Bool)
63
(declare-var relop_test.RelationalOperator14_1_1 Bool)
64
(declare-var relop_test.RelationalOperator15_1_1 Bool)
65
(declare-var relop_test.RelationalOperator16_1_1 Bool)
66
(declare-var relop_test.RelationalOperator17_1_1 Bool)
67
(declare-var relop_test.RelationalOperator1_1_1 Bool)
68
(declare-var relop_test.RelationalOperator2_1_1 Bool)
69
(declare-var relop_test.RelationalOperator3_1_1 Bool)
70
(declare-var relop_test.RelationalOperator4_1_1 Bool)
71
(declare-var relop_test.RelationalOperator5_1_1 Bool)
72
(declare-var relop_test.RelationalOperator6_1_1 Bool)
73
(declare-var relop_test.RelationalOperator7_1_1 Bool)
74
(declare-var relop_test.RelationalOperator8_1_1 Bool)
75
(declare-var relop_test.RelationalOperator9_1_1 Bool)
76
(declare-var relop_test.RelationalOperator_1_1 Bool)
77
(declare-var relop_test.__relop_test_1 Bool)
78
(declare-var relop_test.__relop_test_10 Int)
79
(declare-var relop_test.__relop_test_11 Int)
80
(declare-var relop_test.__relop_test_12 Int)
81
(declare-var relop_test.__relop_test_2 Int)
82
(declare-var relop_test.__relop_test_3 Int)
83
(declare-var relop_test.__relop_test_4 Int)
84
(declare-var relop_test.__relop_test_5 Int)
85
(declare-var relop_test.__relop_test_6 Real)
86
(declare-var relop_test.__relop_test_7 Int)
87
(declare-var relop_test.__relop_test_8 Int)
88
(declare-var relop_test.__relop_test_9 Int)
89
(declare-var relop_test.i_virtual_local Real)
90
(declare-rel relop_test_reset (Bool Bool))
91
(declare-rel relop_test_step (Real Real Int Int Bool Real Real Real Int Int Bool Bool Real Real Int Int Bool Bool Real Real Int Int Bool Bool Real Real Int Int Bool Bool Real Real Int Int Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
92

    
93
(rule (=> 
94
  (and 
95
       
96
       (= relop_test.ni_0._arrow._first_m true)
97
  )
98
  (relop_test_reset relop_test.ni_0._arrow._first_c
99
                    relop_test.ni_0._arrow._first_m)
100
))
101

    
102
(rule (=> 
103
  (and (= relop_test.ni_0._arrow._first_m relop_test.ni_0._arrow._first_c)
104
       (and (= relop_test.__relop_test_1 (ite relop_test.ni_0._arrow._first_m true false))
105
            (= relop_test.ni_0._arrow._first_x false))
106
       (and (or (not (= relop_test.__relop_test_1 true))
107
               (= relop_test.i_virtual_local 0.0))
108
            (or (not (= relop_test.__relop_test_1 false))
109
               (= relop_test.i_virtual_local 1.0))
110
       )
111
       (and (or (not (= relop_test.In30_1_1 true))
112
               (= relop_test.__relop_test_9 1))
113
            (or (not (= relop_test.In30_1_1 false))
114
               (= relop_test.__relop_test_9 0))
115
       )
116
       (and (or (not (= relop_test.In35_1_1 true))
117
               (= relop_test.__relop_test_8 1))
118
            (or (not (= relop_test.In35_1_1 false))
119
               (= relop_test.__relop_test_8 0))
120
       )
121
       (and (or (not (= relop_test.In36_1_1 true))
122
               (= relop_test.__relop_test_7 1))
123
            (or (not (= relop_test.In36_1_1 false))
124
               (= relop_test.__relop_test_7 0))
125
       )
126
       (and (or (not (= relop_test.In5_1_1 true))
127
               (= relop_test.__relop_test_6 1.0))
128
            (or (not (= relop_test.In5_1_1 false))
129
               (= relop_test.__relop_test_6 0.0))
130
       )
131
       (and (or (not (= relop_test.In11_1_1 true))
132
               (= relop_test.__relop_test_5 1))
133
            (or (not (= relop_test.In11_1_1 false))
134
               (= relop_test.__relop_test_5 0))
135
       )
136
       (and (or (not (= relop_test.In12_1_1 true))
137
               (= relop_test.__relop_test_4 1))
138
            (or (not (= relop_test.In12_1_1 false))
139
               (= relop_test.__relop_test_4 0))
140
       )
141
       (and (or (not (= relop_test.In17_1_1 true))
142
               (= relop_test.__relop_test_3 1))
143
            (or (not (= relop_test.In17_1_1 false))
144
               (= relop_test.__relop_test_3 0))
145
       )
146
       (and (or (not (= relop_test.In18_1_1 true))
147
               (= relop_test.__relop_test_2 1))
148
            (or (not (= relop_test.In18_1_1 false))
149
               (= relop_test.__relop_test_2 0))
150
       )
151
       (and (or (not (= relop_test.In23_1_1 true))
152
               (= relop_test.__relop_test_12 1))
153
            (or (not (= relop_test.In23_1_1 false))
154
               (= relop_test.__relop_test_12 0))
155
       )
156
       (and (or (not (= relop_test.In24_1_1 true))
157
               (= relop_test.__relop_test_11 1))
158
            (or (not (= relop_test.In24_1_1 false))
159
               (= relop_test.__relop_test_11 0))
160
       )
161
       (and (or (not (= relop_test.In29_1_1 true))
162
               (= relop_test.__relop_test_10 1))
163
            (or (not (= relop_test.In29_1_1 false))
164
               (= relop_test.__relop_test_10 0))
165
       )
166
       (= relop_test.RelationalOperator_1_1 (<= relop_test.In1_1_1 relop_test.In2_1_1))
167
       (= relop_test.RelationalOperator9_1_1 (< relop_test.In19_1_1 relop_test.In20_1_1))
168
       (= relop_test.RelationalOperator8_1_1 (not (= relop_test.__relop_test_3 relop_test.__relop_test_2)))
169
       (= relop_test.RelationalOperator7_1_1 (not (= relop_test.In15_1_1 relop_test.In16_1_1)))
170
       (= relop_test.RelationalOperator6_1_1 (not (= relop_test.In13_1_1 relop_test.In14_1_1)))
171
       (= relop_test.RelationalOperator5_1_1 (= relop_test.__relop_test_5 relop_test.__relop_test_4))
172
       (= relop_test.RelationalOperator4_1_1 (= relop_test.In9_1_1 relop_test.In10_1_1))
173
       (= relop_test.RelationalOperator3_1_1 (= relop_test.In7_1_1 relop_test.In8_1_1))
174
       (= relop_test.RelationalOperator2_1_1 (<= relop_test.__relop_test_6 relop_test.In6_1_1))
175
       (= relop_test.RelationalOperator1_1_1 (<= relop_test.In3_1_1 relop_test.In4_1_1))
176
       (= relop_test.RelationalOperator17_1_1 (> relop_test.__relop_test_8 relop_test.__relop_test_7))
177
       (= relop_test.RelationalOperator16_1_1 (> relop_test.In33_1_1 relop_test.In34_1_1))
178
       (= relop_test.RelationalOperator15_1_1 (> relop_test.In31_1_1 relop_test.In32_1_1))
179
       (= relop_test.RelationalOperator14_1_1 (>= relop_test.__relop_test_10 relop_test.__relop_test_9))
180
       (= relop_test.RelationalOperator13_1_1 (>= relop_test.In27_1_1 relop_test.In28_1_1))
181
       (= relop_test.RelationalOperator12_1_1 (>= relop_test.In25_1_1 relop_test.In26_1_1))
182
       (= relop_test.RelationalOperator11_1_1 (< relop_test.__relop_test_12 relop_test.__relop_test_11))
183
       (= relop_test.RelationalOperator10_1_1 (< relop_test.In21_1_1 relop_test.In22_1_1))
184
       (= relop_test.Out9_9_1 relop_test.RelationalOperator8_1_1)
185
       (= relop_test.Out8_8_1 relop_test.RelationalOperator7_1_1)
186
       (= relop_test.Out7_7_1 relop_test.RelationalOperator6_1_1)
187
       (= relop_test.Out6_6_1 relop_test.RelationalOperator5_1_1)
188
       (= relop_test.Out5_5_1 relop_test.RelationalOperator4_1_1)
189
       (= relop_test.Out4_4_1 relop_test.RelationalOperator3_1_1)
190
       (= relop_test.Out3_3_1 relop_test.RelationalOperator2_1_1)
191
       (= relop_test.Out2_2_1 relop_test.RelationalOperator1_1_1)
192
       (= relop_test.Out1_1_1 relop_test.RelationalOperator_1_1)
193
       (= relop_test.Out18_18_1 relop_test.RelationalOperator17_1_1)
194
       (= relop_test.Out17_17_1 relop_test.RelationalOperator16_1_1)
195
       (= relop_test.Out16_16_1 relop_test.RelationalOperator15_1_1)
196
       (= relop_test.Out15_15_1 relop_test.RelationalOperator14_1_1)
197
       (= relop_test.Out14_14_1 relop_test.RelationalOperator13_1_1)
198
       (= relop_test.Out13_13_1 relop_test.RelationalOperator12_1_1)
199
       (= relop_test.Out12_12_1 relop_test.RelationalOperator11_1_1)
200
       (= relop_test.Out11_11_1 relop_test.RelationalOperator10_1_1)
201
       (= relop_test.Out10_10_1 relop_test.RelationalOperator9_1_1)
202
       )
203
  (relop_test_step relop_test.In1_1_1
204
                   relop_test.In2_1_1
205
                   relop_test.In3_1_1
206
                   relop_test.In4_1_1
207
                   relop_test.In5_1_1
208
                   relop_test.In6_1_1
209
                   relop_test.In7_1_1
210
                   relop_test.In8_1_1
211
                   relop_test.In9_1_1
212
                   relop_test.In10_1_1
213
                   relop_test.In11_1_1
214
                   relop_test.In12_1_1
215
                   relop_test.In13_1_1
216
                   relop_test.In14_1_1
217
                   relop_test.In15_1_1
218
                   relop_test.In16_1_1
219
                   relop_test.In17_1_1
220
                   relop_test.In18_1_1
221
                   relop_test.In19_1_1
222
                   relop_test.In20_1_1
223
                   relop_test.In21_1_1
224
                   relop_test.In22_1_1
225
                   relop_test.In23_1_1
226
                   relop_test.In24_1_1
227
                   relop_test.In25_1_1
228
                   relop_test.In26_1_1
229
                   relop_test.In27_1_1
230
                   relop_test.In28_1_1
231
                   relop_test.In29_1_1
232
                   relop_test.In30_1_1
233
                   relop_test.In31_1_1
234
                   relop_test.In32_1_1
235
                   relop_test.In33_1_1
236
                   relop_test.In34_1_1
237
                   relop_test.In35_1_1
238
                   relop_test.In36_1_1
239
                   relop_test.Out1_1_1
240
                   relop_test.Out2_2_1
241
                   relop_test.Out3_3_1
242
                   relop_test.Out4_4_1
243
                   relop_test.Out5_5_1
244
                   relop_test.Out6_6_1
245
                   relop_test.Out7_7_1
246
                   relop_test.Out8_8_1
247
                   relop_test.Out9_9_1
248
                   relop_test.Out10_10_1
249
                   relop_test.Out11_11_1
250
                   relop_test.Out12_12_1
251
                   relop_test.Out13_13_1
252
                   relop_test.Out14_14_1
253
                   relop_test.Out15_15_1
254
                   relop_test.Out16_16_1
255
                   relop_test.Out17_17_1
256
                   relop_test.Out18_18_1
257
                   relop_test.ni_0._arrow._first_c
258
                   relop_test.ni_0._arrow._first_x)
259
))
260