Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_product_elementwise_test / product_elementwise_test.smt2 @ 6c3ea955

History | View | Annotate | Download (14.3 KB)

1
; product_elementwise_test
2
(declare-var product_elementwise_test.In1_1_1 Real)
3
(declare-var product_elementwise_test.In2_1_1 Real)
4
(declare-var product_elementwise_test.In3_1_1 Real)
5
(declare-var product_elementwise_test.In3_1_2 Real)
6
(declare-var product_elementwise_test.In4_1_1 Real)
7
(declare-var product_elementwise_test.In4_1_2 Real)
8
(declare-var product_elementwise_test.In5_1_1 Real)
9
(declare-var product_elementwise_test.In5_1_2 Real)
10
(declare-var product_elementwise_test.In5_1_3 Real)
11
(declare-var product_elementwise_test.In5_1_4 Real)
12
(declare-var product_elementwise_test.In6_1_1 Real)
13
(declare-var product_elementwise_test.In6_1_2 Real)
14
(declare-var product_elementwise_test.In6_1_3 Real)
15
(declare-var product_elementwise_test.In6_1_4 Real)
16
(declare-var product_elementwise_test.In7_1_1 Real)
17
(declare-var product_elementwise_test.In8_1_1 Real)
18
(declare-var product_elementwise_test.In9_1_1 Real)
19
(declare-var product_elementwise_test.In10_1_1 Real)
20
(declare-var product_elementwise_test.In11_1_1 Real)
21
(declare-var product_elementwise_test.In11_1_2 Real)
22
(declare-var product_elementwise_test.In12_1_1 Real)
23
(declare-var product_elementwise_test.In12_1_2 Real)
24
(declare-var product_elementwise_test.In13_1_1 Real)
25
(declare-var product_elementwise_test.In13_1_2 Real)
26
(declare-var product_elementwise_test.In14_1_1 Real)
27
(declare-var product_elementwise_test.In14_1_2 Real)
28
(declare-var product_elementwise_test.In15_1_1 Real)
29
(declare-var product_elementwise_test.In15_1_2 Real)
30
(declare-var product_elementwise_test.In15_1_3 Real)
31
(declare-var product_elementwise_test.In15_1_4 Real)
32
(declare-var product_elementwise_test.In15_1_5 Real)
33
(declare-var product_elementwise_test.In15_1_6 Real)
34
(declare-var product_elementwise_test.In16_1_1 Real)
35
(declare-var product_elementwise_test.In16_1_2 Real)
36
(declare-var product_elementwise_test.In16_1_3 Real)
37
(declare-var product_elementwise_test.In16_1_4 Real)
38
(declare-var product_elementwise_test.In16_1_5 Real)
39
(declare-var product_elementwise_test.In16_1_6 Real)
40
(declare-var product_elementwise_test.In17_1_1 Real)
41
(declare-var product_elementwise_test.In17_1_2 Real)
42
(declare-var product_elementwise_test.In17_1_3 Real)
43
(declare-var product_elementwise_test.In17_1_4 Real)
44
(declare-var product_elementwise_test.In17_1_5 Real)
45
(declare-var product_elementwise_test.In17_1_6 Real)
46
(declare-var product_elementwise_test.In18_1_1 Real)
47
(declare-var product_elementwise_test.In18_1_2 Real)
48
(declare-var product_elementwise_test.In18_1_3 Real)
49
(declare-var product_elementwise_test.In18_1_4 Real)
50
(declare-var product_elementwise_test.In18_1_5 Real)
51
(declare-var product_elementwise_test.In18_1_6 Real)
52
(declare-var product_elementwise_test.Out1_1_1 Real)
53
(declare-var product_elementwise_test.Out2_2_1 Real)
54
(declare-var product_elementwise_test.Out2_2_2 Real)
55
(declare-var product_elementwise_test.Out3_3_1 Real)
56
(declare-var product_elementwise_test.Out3_3_2 Real)
57
(declare-var product_elementwise_test.Out3_3_3 Real)
58
(declare-var product_elementwise_test.Out3_3_4 Real)
59
(declare-var product_elementwise_test.Out4_4_1 Real)
60
(declare-var product_elementwise_test.Out5_5_1 Real)
61
(declare-var product_elementwise_test.Out5_5_2 Real)
62
(declare-var product_elementwise_test.Out6_6_1 Real)
63
(declare-var product_elementwise_test.Out6_6_2 Real)
64
(declare-var product_elementwise_test.Out6_6_3 Real)
65
(declare-var product_elementwise_test.Out6_6_4 Real)
66
(declare-var product_elementwise_test.Out6_6_5 Real)
67
(declare-var product_elementwise_test.Out6_6_6 Real)
68
(declare-var product_elementwise_test.ni_0._arrow._first_c Bool)
69
(declare-var product_elementwise_test.ni_0._arrow._first_m Bool)
70
(declare-var product_elementwise_test.ni_0._arrow._first_x Bool)
71
(declare-var product_elementwise_test.Product1_1_1 Real)
72
(declare-var product_elementwise_test.Product1_1_2 Real)
73
(declare-var product_elementwise_test.Product2_1_1 Real)
74
(declare-var product_elementwise_test.Product2_1_2 Real)
75
(declare-var product_elementwise_test.Product2_1_3 Real)
76
(declare-var product_elementwise_test.Product2_1_4 Real)
77
(declare-var product_elementwise_test.Product3_1_1 Real)
78
(declare-var product_elementwise_test.Product4_1_1 Real)
79
(declare-var product_elementwise_test.Product4_1_2 Real)
80
(declare-var product_elementwise_test.Product5_1_1 Real)
81
(declare-var product_elementwise_test.Product5_1_2 Real)
82
(declare-var product_elementwise_test.Product5_1_3 Real)
83
(declare-var product_elementwise_test.Product5_1_4 Real)
84
(declare-var product_elementwise_test.Product5_1_5 Real)
85
(declare-var product_elementwise_test.Product5_1_6 Real)
86
(declare-var product_elementwise_test.Product_1_1 Real)
87
(declare-var product_elementwise_test.__product_elementwise_test_1 Bool)
88
(declare-var product_elementwise_test.i_virtual_local Real)
89
(declare-rel product_elementwise_test_reset (Bool Bool))
90
(declare-rel product_elementwise_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 Bool Bool))
91

    
92
(rule (=> 
93
  (and 
94
       
95
       (= product_elementwise_test.ni_0._arrow._first_m true)
96
  )
97
  (product_elementwise_test_reset product_elementwise_test.ni_0._arrow._first_c
98
                                  product_elementwise_test.ni_0._arrow._first_m)
99
))
100

    
101
(rule (=> 
102
  (and (= product_elementwise_test.ni_0._arrow._first_m product_elementwise_test.ni_0._arrow._first_c)
103
       (and (= product_elementwise_test.__product_elementwise_test_1 (ite product_elementwise_test.ni_0._arrow._first_m true false))
104
            (= product_elementwise_test.ni_0._arrow._first_x false))
105
       (and (or (not (= product_elementwise_test.__product_elementwise_test_1 true))
106
               (= product_elementwise_test.i_virtual_local 0.0))
107
            (or (not (= product_elementwise_test.__product_elementwise_test_1 false))
108
               (= product_elementwise_test.i_virtual_local 1.0))
109
       )
110
       (= product_elementwise_test.Product_1_1 (* product_elementwise_test.In1_1_1 product_elementwise_test.In2_1_1))
111
       (= product_elementwise_test.Product5_1_6 (* (* (* product_elementwise_test.In15_1_6 product_elementwise_test.In16_1_6) product_elementwise_test.In17_1_6) product_elementwise_test.In18_1_6))
112
       (= product_elementwise_test.Product5_1_5 (* (* (* product_elementwise_test.In15_1_5 product_elementwise_test.In16_1_5) product_elementwise_test.In17_1_5) product_elementwise_test.In18_1_5))
113
       (= product_elementwise_test.Product5_1_4 (* (* (* product_elementwise_test.In15_1_4 product_elementwise_test.In16_1_4) product_elementwise_test.In17_1_4) product_elementwise_test.In18_1_4))
114
       (= product_elementwise_test.Product5_1_3 (* (* (* product_elementwise_test.In15_1_3 product_elementwise_test.In16_1_3) product_elementwise_test.In17_1_3) product_elementwise_test.In18_1_3))
115
       (= product_elementwise_test.Product5_1_2 (* (* (* product_elementwise_test.In15_1_2 product_elementwise_test.In16_1_2) product_elementwise_test.In17_1_2) product_elementwise_test.In18_1_2))
116
       (= product_elementwise_test.Product5_1_1 (* (* (* product_elementwise_test.In15_1_1 product_elementwise_test.In16_1_1) product_elementwise_test.In17_1_1) product_elementwise_test.In18_1_1))
117
       (= product_elementwise_test.Product4_1_2 (* (* (* product_elementwise_test.In11_1_2 product_elementwise_test.In12_1_2) product_elementwise_test.In13_1_2) product_elementwise_test.In14_1_2))
118
       (= product_elementwise_test.Product4_1_1 (* (* (* product_elementwise_test.In11_1_1 product_elementwise_test.In12_1_1) product_elementwise_test.In13_1_1) product_elementwise_test.In14_1_1))
119
       (= product_elementwise_test.Product3_1_1 (* (* (* product_elementwise_test.In7_1_1 product_elementwise_test.In8_1_1) product_elementwise_test.In9_1_1) product_elementwise_test.In10_1_1))
120
       (= product_elementwise_test.Product2_1_4 (* (div 1.0 product_elementwise_test.In5_1_4) product_elementwise_test.In6_1_4))
121
       (= product_elementwise_test.Product2_1_3 (* (div 1.0 product_elementwise_test.In5_1_3) product_elementwise_test.In6_1_3))
122
       (= product_elementwise_test.Product2_1_2 (* (div 1.0 product_elementwise_test.In5_1_2) product_elementwise_test.In6_1_2))
123
       (= product_elementwise_test.Product2_1_1 (* (div 1.0 product_elementwise_test.In5_1_1) product_elementwise_test.In6_1_1))
124
       (= product_elementwise_test.Product1_1_2 (div product_elementwise_test.In3_1_2 product_elementwise_test.In4_1_2))
125
       (= product_elementwise_test.Product1_1_1 (div product_elementwise_test.In3_1_1 product_elementwise_test.In4_1_1))
126
       (= product_elementwise_test.Out6_6_6 product_elementwise_test.Product5_1_6)
127
       (= product_elementwise_test.Out6_6_5 product_elementwise_test.Product5_1_5)
128
       (= product_elementwise_test.Out6_6_4 product_elementwise_test.Product5_1_4)
129
       (= product_elementwise_test.Out6_6_3 product_elementwise_test.Product5_1_3)
130
       (= product_elementwise_test.Out6_6_2 product_elementwise_test.Product5_1_2)
131
       (= product_elementwise_test.Out6_6_1 product_elementwise_test.Product5_1_1)
132
       (= product_elementwise_test.Out5_5_2 product_elementwise_test.Product4_1_2)
133
       (= product_elementwise_test.Out5_5_1 product_elementwise_test.Product4_1_1)
134
       (= product_elementwise_test.Out4_4_1 product_elementwise_test.Product3_1_1)
135
       (= product_elementwise_test.Out3_3_4 product_elementwise_test.Product2_1_4)
136
       (= product_elementwise_test.Out3_3_3 product_elementwise_test.Product2_1_3)
137
       (= product_elementwise_test.Out3_3_2 product_elementwise_test.Product2_1_2)
138
       (= product_elementwise_test.Out3_3_1 product_elementwise_test.Product2_1_1)
139
       (= product_elementwise_test.Out2_2_2 product_elementwise_test.Product1_1_2)
140
       (= product_elementwise_test.Out2_2_1 product_elementwise_test.Product1_1_1)
141
       (= product_elementwise_test.Out1_1_1 product_elementwise_test.Product_1_1)
142
       )
143
  (product_elementwise_test_step product_elementwise_test.In1_1_1
144
                                 product_elementwise_test.In2_1_1
145
                                 product_elementwise_test.In3_1_1
146
                                 product_elementwise_test.In3_1_2
147
                                 product_elementwise_test.In4_1_1
148
                                 product_elementwise_test.In4_1_2
149
                                 product_elementwise_test.In5_1_1
150
                                 product_elementwise_test.In5_1_2
151
                                 product_elementwise_test.In5_1_3
152
                                 product_elementwise_test.In5_1_4
153
                                 product_elementwise_test.In6_1_1
154
                                 product_elementwise_test.In6_1_2
155
                                 product_elementwise_test.In6_1_3
156
                                 product_elementwise_test.In6_1_4
157
                                 product_elementwise_test.In7_1_1
158
                                 product_elementwise_test.In8_1_1
159
                                 product_elementwise_test.In9_1_1
160
                                 product_elementwise_test.In10_1_1
161
                                 product_elementwise_test.In11_1_1
162
                                 product_elementwise_test.In11_1_2
163
                                 product_elementwise_test.In12_1_1
164
                                 product_elementwise_test.In12_1_2
165
                                 product_elementwise_test.In13_1_1
166
                                 product_elementwise_test.In13_1_2
167
                                 product_elementwise_test.In14_1_1
168
                                 product_elementwise_test.In14_1_2
169
                                 product_elementwise_test.In15_1_1
170
                                 product_elementwise_test.In15_1_2
171
                                 product_elementwise_test.In15_1_3
172
                                 product_elementwise_test.In15_1_4
173
                                 product_elementwise_test.In15_1_5
174
                                 product_elementwise_test.In15_1_6
175
                                 product_elementwise_test.In16_1_1
176
                                 product_elementwise_test.In16_1_2
177
                                 product_elementwise_test.In16_1_3
178
                                 product_elementwise_test.In16_1_4
179
                                 product_elementwise_test.In16_1_5
180
                                 product_elementwise_test.In16_1_6
181
                                 product_elementwise_test.In17_1_1
182
                                 product_elementwise_test.In17_1_2
183
                                 product_elementwise_test.In17_1_3
184
                                 product_elementwise_test.In17_1_4
185
                                 product_elementwise_test.In17_1_5
186
                                 product_elementwise_test.In17_1_6
187
                                 product_elementwise_test.In18_1_1
188
                                 product_elementwise_test.In18_1_2
189
                                 product_elementwise_test.In18_1_3
190
                                 product_elementwise_test.In18_1_4
191
                                 product_elementwise_test.In18_1_5
192
                                 product_elementwise_test.In18_1_6
193
                                 product_elementwise_test.Out1_1_1
194
                                 product_elementwise_test.Out2_2_1
195
                                 product_elementwise_test.Out2_2_2
196
                                 product_elementwise_test.Out3_3_1
197
                                 product_elementwise_test.Out3_3_2
198
                                 product_elementwise_test.Out3_3_3
199
                                 product_elementwise_test.Out3_3_4
200
                                 product_elementwise_test.Out4_4_1
201
                                 product_elementwise_test.Out5_5_1
202
                                 product_elementwise_test.Out5_5_2
203
                                 product_elementwise_test.Out6_6_1
204
                                 product_elementwise_test.Out6_6_2
205
                                 product_elementwise_test.Out6_6_3
206
                                 product_elementwise_test.Out6_6_4
207
                                 product_elementwise_test.Out6_6_5
208
                                 product_elementwise_test.Out6_6_6
209
                                 product_elementwise_test.ni_0._arrow._first_c
210
                                 product_elementwise_test.ni_0._arrow._first_x)
211
))
212