Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_product_collapse_test / product_collapse_test.smt2 @ 6c3ea955

History | View | Annotate | Download (15 KB)

1
; product_collapse_test
2
(declare-var product_collapse_test.In1_1_1 Real)
3
(declare-var product_collapse_test.In3_1_1 Real)
4
(declare-var product_collapse_test.In3_1_2 Real)
5
(declare-var product_collapse_test.In3_1_3 Real)
6
(declare-var product_collapse_test.In3_1_4 Real)
7
(declare-var product_collapse_test.In3_1_5 Real)
8
(declare-var product_collapse_test.In3_1_6 Real)
9
(declare-var product_collapse_test.In2_1_1 Real)
10
(declare-var product_collapse_test.In2_1_2 Real)
11
(declare-var product_collapse_test.In2_1_3 Real)
12
(declare-var product_collapse_test.In7_1_1 Real)
13
(declare-var product_collapse_test.In8_1_1 Real)
14
(declare-var product_collapse_test.In8_1_2 Real)
15
(declare-var product_collapse_test.In8_1_3 Real)
16
(declare-var product_collapse_test.In9_1_1 Real)
17
(declare-var product_collapse_test.In9_1_2 Real)
18
(declare-var product_collapse_test.In9_1_3 Real)
19
(declare-var product_collapse_test.In9_1_4 Real)
20
(declare-var product_collapse_test.In9_1_5 Real)
21
(declare-var product_collapse_test.In9_1_6 Real)
22
(declare-var product_collapse_test.In4_1_1 Real)
23
(declare-var product_collapse_test.In6_1_1 Real)
24
(declare-var product_collapse_test.In6_1_2 Real)
25
(declare-var product_collapse_test.In6_1_3 Real)
26
(declare-var product_collapse_test.In6_1_4 Real)
27
(declare-var product_collapse_test.In6_1_5 Real)
28
(declare-var product_collapse_test.In6_1_6 Real)
29
(declare-var product_collapse_test.In5_1_1 Real)
30
(declare-var product_collapse_test.In5_1_2 Real)
31
(declare-var product_collapse_test.In5_1_3 Real)
32
(declare-var product_collapse_test.In10_1_1 Real)
33
(declare-var product_collapse_test.In10_1_2 Real)
34
(declare-var product_collapse_test.In10_1_3 Real)
35
(declare-var product_collapse_test.In10_1_4 Real)
36
(declare-var product_collapse_test.In10_1_5 Real)
37
(declare-var product_collapse_test.In10_1_6 Real)
38
(declare-var product_collapse_test.In11_1_1 Real)
39
(declare-var product_collapse_test.In12_1_1 Real)
40
(declare-var product_collapse_test.In12_1_2 Real)
41
(declare-var product_collapse_test.In12_1_3 Real)
42
(declare-var product_collapse_test.In13_1_1 Real)
43
(declare-var product_collapse_test.In13_1_2 Real)
44
(declare-var product_collapse_test.In13_1_3 Real)
45
(declare-var product_collapse_test.In13_1_4 Real)
46
(declare-var product_collapse_test.In13_1_5 Real)
47
(declare-var product_collapse_test.In13_1_6 Real)
48
(declare-var product_collapse_test.In14_1_1 Real)
49
(declare-var product_collapse_test.In14_1_2 Real)
50
(declare-var product_collapse_test.In14_1_3 Real)
51
(declare-var product_collapse_test.In14_1_4 Real)
52
(declare-var product_collapse_test.In14_1_5 Real)
53
(declare-var product_collapse_test.In14_1_6 Real)
54
(declare-var product_collapse_test.Out1_1_1 Real)
55
(declare-var product_collapse_test.Out3_2_1 Real)
56
(declare-var product_collapse_test.Out2_3_1 Real)
57
(declare-var product_collapse_test.Out7_4_1 Real)
58
(declare-var product_collapse_test.Out8_5_1 Real)
59
(declare-var product_collapse_test.Out9_6_1 Real)
60
(declare-var product_collapse_test.Out9_6_2 Real)
61
(declare-var product_collapse_test.Out9_6_3 Real)
62
(declare-var product_collapse_test.Out4_7_1 Real)
63
(declare-var product_collapse_test.Out6_8_1 Real)
64
(declare-var product_collapse_test.Out5_9_1 Real)
65
(declare-var product_collapse_test.Out10_10_1 Real)
66
(declare-var product_collapse_test.Out10_10_2 Real)
67
(declare-var product_collapse_test.Out11_11_1 Real)
68
(declare-var product_collapse_test.Out12_12_1 Real)
69
(declare-var product_collapse_test.Out13_13_1 Real)
70
(declare-var product_collapse_test.Out13_13_2 Real)
71
(declare-var product_collapse_test.Out13_13_3 Real)
72
(declare-var product_collapse_test.Out14_14_1 Real)
73
(declare-var product_collapse_test.Out14_14_2 Real)
74
(declare-var product_collapse_test.ni_0._arrow._first_c Bool)
75
(declare-var product_collapse_test.ni_0._arrow._first_m Bool)
76
(declare-var product_collapse_test.ni_0._arrow._first_x Bool)
77
(declare-var product_collapse_test.Product10_1_1 Real)
78
(declare-var product_collapse_test.Product10_1_2 Real)
79
(declare-var product_collapse_test.Product11_1_1 Real)
80
(declare-var product_collapse_test.Product11_1_2 Real)
81
(declare-var product_collapse_test.Product12_1_1 Real)
82
(declare-var product_collapse_test.Product13_1_1 Real)
83
(declare-var product_collapse_test.Product14_1_1 Real)
84
(declare-var product_collapse_test.Product14_1_2 Real)
85
(declare-var product_collapse_test.Product14_1_3 Real)
86
(declare-var product_collapse_test.Product1_1_1 Real)
87
(declare-var product_collapse_test.Product2_1_1 Real)
88
(declare-var product_collapse_test.Product3_1_1 Real)
89
(declare-var product_collapse_test.Product4_1_1 Real)
90
(declare-var product_collapse_test.Product5_1_1 Real)
91
(declare-var product_collapse_test.Product6_1_1 Real)
92
(declare-var product_collapse_test.Product7_1_1 Real)
93
(declare-var product_collapse_test.Product8_1_1 Real)
94
(declare-var product_collapse_test.Product9_1_1 Real)
95
(declare-var product_collapse_test.Product9_1_2 Real)
96
(declare-var product_collapse_test.Product9_1_3 Real)
97
(declare-var product_collapse_test.__product_collapse_test_1 Bool)
98
(declare-var product_collapse_test.i_virtual_local Real)
99
(declare-rel product_collapse_test_reset (Bool Bool))
100
(declare-rel product_collapse_test_step (Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Bool Bool))
101

    
102
(rule (=> 
103
  (and 
104
       
105
       (= product_collapse_test.ni_0._arrow._first_m true)
106
  )
107
  (product_collapse_test_reset product_collapse_test.ni_0._arrow._first_c
108
                               product_collapse_test.ni_0._arrow._first_m)
109
))
110

    
111
(rule (=> 
112
  (and (= product_collapse_test.ni_0._arrow._first_m product_collapse_test.ni_0._arrow._first_c)
113
       (and (= product_collapse_test.__product_collapse_test_1 (ite product_collapse_test.ni_0._arrow._first_m true false))
114
            (= product_collapse_test.ni_0._arrow._first_x false))
115
       (and (or (not (= product_collapse_test.__product_collapse_test_1 true))
116
               (= product_collapse_test.i_virtual_local 0.0))
117
            (or (not (= product_collapse_test.__product_collapse_test_1 false))
118
               (= product_collapse_test.i_virtual_local 1.0))
119
       )
120
       (= product_collapse_test.Product9_1_3 (* product_collapse_test.In9_1_3 product_collapse_test.In9_1_6))
121
       (= product_collapse_test.Product9_1_2 (* product_collapse_test.In9_1_2 product_collapse_test.In9_1_5))
122
       (= product_collapse_test.Product9_1_1 (* product_collapse_test.In9_1_1 product_collapse_test.In9_1_4))
123
       (= product_collapse_test.Product8_1_1 (* (* product_collapse_test.In8_1_1 product_collapse_test.In8_1_2) product_collapse_test.In8_1_3))
124
       (= product_collapse_test.Product7_1_1 product_collapse_test.In7_1_1)
125
       (= product_collapse_test.Product6_1_1 (* (* (* (* (* (div 1.0 product_collapse_test.In6_1_1) (div 1.0 product_collapse_test.In6_1_2)) (div 1.0 product_collapse_test.In6_1_3)) (div 1.0 product_collapse_test.In6_1_4)) (div 1.0 product_collapse_test.In6_1_5)) (div 1.0 product_collapse_test.In6_1_6)))
126
       (= product_collapse_test.Product5_1_1 (* (* (div 1.0 product_collapse_test.In5_1_1) (div 1.0 product_collapse_test.In5_1_2)) (div 1.0 product_collapse_test.In5_1_3)))
127
       (= product_collapse_test.Product4_1_1 (div 1.0 product_collapse_test.In4_1_1))
128
       (= product_collapse_test.Product3_1_1 (* (* (* (* (* product_collapse_test.In3_1_1 product_collapse_test.In3_1_2) product_collapse_test.In3_1_3) product_collapse_test.In3_1_4) product_collapse_test.In3_1_5) product_collapse_test.In3_1_6))
129
       (= product_collapse_test.Product2_1_1 (* (* product_collapse_test.In2_1_1 product_collapse_test.In2_1_2) product_collapse_test.In2_1_3))
130
       (= product_collapse_test.Product1_1_1 product_collapse_test.In1_1_1)
131
       (= product_collapse_test.Product14_1_3 (* (div 1.0 product_collapse_test.In13_1_3) (div 1.0 product_collapse_test.In13_1_6)))
132
       (= product_collapse_test.Product14_1_2 (* (div 1.0 product_collapse_test.In13_1_2) (div 1.0 product_collapse_test.In13_1_5)))
133
       (= product_collapse_test.Product14_1_1 (* (div 1.0 product_collapse_test.In13_1_1) (div 1.0 product_collapse_test.In13_1_4)))
134
       (= product_collapse_test.Product13_1_1 (* (* (div 1.0 product_collapse_test.In12_1_1) (div 1.0 product_collapse_test.In12_1_2)) (div 1.0 product_collapse_test.In12_1_3)))
135
       (= product_collapse_test.Product12_1_1 (div 1.0 product_collapse_test.In11_1_1))
136
       (= product_collapse_test.Product11_1_2 (* (* (div 1.0 product_collapse_test.In14_1_4) (div 1.0 product_collapse_test.In14_1_5)) (div 1.0 product_collapse_test.In14_1_6)))
137
       (= product_collapse_test.Product11_1_1 (* (* (div 1.0 product_collapse_test.In14_1_1) (div 1.0 product_collapse_test.In14_1_2)) (div 1.0 product_collapse_test.In14_1_3)))
138
       (= product_collapse_test.Product10_1_2 (* (* product_collapse_test.In10_1_4 product_collapse_test.In10_1_5) product_collapse_test.In10_1_6))
139
       (= product_collapse_test.Product10_1_1 (* (* product_collapse_test.In10_1_1 product_collapse_test.In10_1_2) product_collapse_test.In10_1_3))
140
       (= product_collapse_test.Out9_6_3 product_collapse_test.Product9_1_3)
141
       (= product_collapse_test.Out9_6_2 product_collapse_test.Product9_1_2)
142
       (= product_collapse_test.Out9_6_1 product_collapse_test.Product9_1_1)
143
       (= product_collapse_test.Out8_5_1 product_collapse_test.Product8_1_1)
144
       (= product_collapse_test.Out7_4_1 product_collapse_test.Product7_1_1)
145
       (= product_collapse_test.Out6_8_1 product_collapse_test.Product6_1_1)
146
       (= product_collapse_test.Out5_9_1 product_collapse_test.Product5_1_1)
147
       (= product_collapse_test.Out4_7_1 product_collapse_test.Product4_1_1)
148
       (= product_collapse_test.Out3_2_1 product_collapse_test.Product3_1_1)
149
       (= product_collapse_test.Out2_3_1 product_collapse_test.Product2_1_1)
150
       (= product_collapse_test.Out1_1_1 product_collapse_test.Product1_1_1)
151
       (= product_collapse_test.Out14_14_2 product_collapse_test.Product11_1_2)
152
       (= product_collapse_test.Out14_14_1 product_collapse_test.Product11_1_1)
153
       (= product_collapse_test.Out13_13_3 product_collapse_test.Product14_1_3)
154
       (= product_collapse_test.Out13_13_2 product_collapse_test.Product14_1_2)
155
       (= product_collapse_test.Out13_13_1 product_collapse_test.Product14_1_1)
156
       (= product_collapse_test.Out12_12_1 product_collapse_test.Product13_1_1)
157
       (= product_collapse_test.Out11_11_1 product_collapse_test.Product12_1_1)
158
       (= product_collapse_test.Out10_10_2 product_collapse_test.Product10_1_2)
159
       (= product_collapse_test.Out10_10_1 product_collapse_test.Product10_1_1)
160
       )
161
  (product_collapse_test_step product_collapse_test.In1_1_1
162
                              product_collapse_test.In3_1_1
163
                              product_collapse_test.In3_1_2
164
                              product_collapse_test.In3_1_3
165
                              product_collapse_test.In3_1_4
166
                              product_collapse_test.In3_1_5
167
                              product_collapse_test.In3_1_6
168
                              product_collapse_test.In2_1_1
169
                              product_collapse_test.In2_1_2
170
                              product_collapse_test.In2_1_3
171
                              product_collapse_test.In7_1_1
172
                              product_collapse_test.In8_1_1
173
                              product_collapse_test.In8_1_2
174
                              product_collapse_test.In8_1_3
175
                              product_collapse_test.In9_1_1
176
                              product_collapse_test.In9_1_2
177
                              product_collapse_test.In9_1_3
178
                              product_collapse_test.In9_1_4
179
                              product_collapse_test.In9_1_5
180
                              product_collapse_test.In9_1_6
181
                              product_collapse_test.In4_1_1
182
                              product_collapse_test.In6_1_1
183
                              product_collapse_test.In6_1_2
184
                              product_collapse_test.In6_1_3
185
                              product_collapse_test.In6_1_4
186
                              product_collapse_test.In6_1_5
187
                              product_collapse_test.In6_1_6
188
                              product_collapse_test.In5_1_1
189
                              product_collapse_test.In5_1_2
190
                              product_collapse_test.In5_1_3
191
                              product_collapse_test.In10_1_1
192
                              product_collapse_test.In10_1_2
193
                              product_collapse_test.In10_1_3
194
                              product_collapse_test.In10_1_4
195
                              product_collapse_test.In10_1_5
196
                              product_collapse_test.In10_1_6
197
                              product_collapse_test.In11_1_1
198
                              product_collapse_test.In12_1_1
199
                              product_collapse_test.In12_1_2
200
                              product_collapse_test.In12_1_3
201
                              product_collapse_test.In13_1_1
202
                              product_collapse_test.In13_1_2
203
                              product_collapse_test.In13_1_3
204
                              product_collapse_test.In13_1_4
205
                              product_collapse_test.In13_1_5
206
                              product_collapse_test.In13_1_6
207
                              product_collapse_test.In14_1_1
208
                              product_collapse_test.In14_1_2
209
                              product_collapse_test.In14_1_3
210
                              product_collapse_test.In14_1_4
211
                              product_collapse_test.In14_1_5
212
                              product_collapse_test.In14_1_6
213
                              product_collapse_test.Out1_1_1
214
                              product_collapse_test.Out3_2_1
215
                              product_collapse_test.Out2_3_1
216
                              product_collapse_test.Out7_4_1
217
                              product_collapse_test.Out8_5_1
218
                              product_collapse_test.Out9_6_1
219
                              product_collapse_test.Out9_6_2
220
                              product_collapse_test.Out9_6_3
221
                              product_collapse_test.Out4_7_1
222
                              product_collapse_test.Out6_8_1
223
                              product_collapse_test.Out5_9_1
224
                              product_collapse_test.Out10_10_1
225
                              product_collapse_test.Out10_10_2
226
                              product_collapse_test.Out11_11_1
227
                              product_collapse_test.Out12_12_1
228
                              product_collapse_test.Out13_13_1
229
                              product_collapse_test.Out13_13_2
230
                              product_collapse_test.Out13_13_3
231
                              product_collapse_test.Out14_14_1
232
                              product_collapse_test.Out14_14_2
233
                              product_collapse_test.ni_0._arrow._first_c
234
                              product_collapse_test.ni_0._arrow._first_x)
235
))
236