Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_logic_expand_2_test / logic_expand_2_test.smt2 @ 6c3ea955

History | View | Annotate | Download (14.6 KB)

1
; logic_expand_2_test
2
(declare-var logic_expand_2_test.In1_1_1 Bool)
3
(declare-var logic_expand_2_test.In2_1_1 Bool)
4
(declare-var logic_expand_2_test.In2_1_2 Bool)
5
(declare-var logic_expand_2_test.In2_1_3 Bool)
6
(declare-var logic_expand_2_test.In2_1_4 Bool)
7
(declare-var logic_expand_2_test.In2_1_5 Bool)
8
(declare-var logic_expand_2_test.In2_1_6 Bool)
9
(declare-var logic_expand_2_test.In3_1_1 Bool)
10
(declare-var logic_expand_2_test.In4_1_1 Bool)
11
(declare-var logic_expand_2_test.In4_1_2 Bool)
12
(declare-var logic_expand_2_test.In4_1_3 Bool)
13
(declare-var logic_expand_2_test.In4_1_4 Bool)
14
(declare-var logic_expand_2_test.In4_1_5 Bool)
15
(declare-var logic_expand_2_test.In4_1_6 Bool)
16
(declare-var logic_expand_2_test.In5_1_1 Bool)
17
(declare-var logic_expand_2_test.In6_1_1 Bool)
18
(declare-var logic_expand_2_test.In6_1_2 Bool)
19
(declare-var logic_expand_2_test.In6_1_3 Bool)
20
(declare-var logic_expand_2_test.In6_1_4 Bool)
21
(declare-var logic_expand_2_test.In6_1_5 Bool)
22
(declare-var logic_expand_2_test.In6_1_6 Bool)
23
(declare-var logic_expand_2_test.In7_1_1 Bool)
24
(declare-var logic_expand_2_test.In8_1_1 Bool)
25
(declare-var logic_expand_2_test.In9_1_1 Bool)
26
(declare-var logic_expand_2_test.In9_1_2 Bool)
27
(declare-var logic_expand_2_test.In9_1_3 Bool)
28
(declare-var logic_expand_2_test.In9_1_4 Bool)
29
(declare-var logic_expand_2_test.In9_1_5 Bool)
30
(declare-var logic_expand_2_test.In9_1_6 Bool)
31
(declare-var logic_expand_2_test.In10_1_1 Bool)
32
(declare-var logic_expand_2_test.In10_1_2 Bool)
33
(declare-var logic_expand_2_test.In10_1_3 Bool)
34
(declare-var logic_expand_2_test.In10_1_4 Bool)
35
(declare-var logic_expand_2_test.In10_1_5 Bool)
36
(declare-var logic_expand_2_test.In10_1_6 Bool)
37
(declare-var logic_expand_2_test.In11_1_1 Bool)
38
(declare-var logic_expand_2_test.In12_1_1 Bool)
39
(declare-var logic_expand_2_test.Out1_1_1 Bool)
40
(declare-var logic_expand_2_test.Out1_1_2 Bool)
41
(declare-var logic_expand_2_test.Out1_1_3 Bool)
42
(declare-var logic_expand_2_test.Out1_1_4 Bool)
43
(declare-var logic_expand_2_test.Out1_1_5 Bool)
44
(declare-var logic_expand_2_test.Out1_1_6 Bool)
45
(declare-var logic_expand_2_test.Out2_2_1 Bool)
46
(declare-var logic_expand_2_test.Out2_2_2 Bool)
47
(declare-var logic_expand_2_test.Out2_2_3 Bool)
48
(declare-var logic_expand_2_test.Out2_2_4 Bool)
49
(declare-var logic_expand_2_test.Out2_2_5 Bool)
50
(declare-var logic_expand_2_test.Out2_2_6 Bool)
51
(declare-var logic_expand_2_test.Out3_3_1 Bool)
52
(declare-var logic_expand_2_test.Out3_3_2 Bool)
53
(declare-var logic_expand_2_test.Out3_3_3 Bool)
54
(declare-var logic_expand_2_test.Out3_3_4 Bool)
55
(declare-var logic_expand_2_test.Out3_3_5 Bool)
56
(declare-var logic_expand_2_test.Out3_3_6 Bool)
57
(declare-var logic_expand_2_test.Out4_4_1 Bool)
58
(declare-var logic_expand_2_test.Out4_4_2 Bool)
59
(declare-var logic_expand_2_test.Out4_4_3 Bool)
60
(declare-var logic_expand_2_test.Out4_4_4 Bool)
61
(declare-var logic_expand_2_test.Out4_4_5 Bool)
62
(declare-var logic_expand_2_test.Out4_4_6 Bool)
63
(declare-var logic_expand_2_test.ni_0._arrow._first_c Bool)
64
(declare-var logic_expand_2_test.ni_0._arrow._first_m Bool)
65
(declare-var logic_expand_2_test.ni_0._arrow._first_x Bool)
66
(declare-var logic_expand_2_test.LogicalOperator1_1_1 Bool)
67
(declare-var logic_expand_2_test.LogicalOperator1_1_2 Bool)
68
(declare-var logic_expand_2_test.LogicalOperator1_1_3 Bool)
69
(declare-var logic_expand_2_test.LogicalOperator1_1_4 Bool)
70
(declare-var logic_expand_2_test.LogicalOperator1_1_5 Bool)
71
(declare-var logic_expand_2_test.LogicalOperator1_1_6 Bool)
72
(declare-var logic_expand_2_test.LogicalOperator2_1_1 Bool)
73
(declare-var logic_expand_2_test.LogicalOperator2_1_2 Bool)
74
(declare-var logic_expand_2_test.LogicalOperator2_1_3 Bool)
75
(declare-var logic_expand_2_test.LogicalOperator2_1_4 Bool)
76
(declare-var logic_expand_2_test.LogicalOperator2_1_5 Bool)
77
(declare-var logic_expand_2_test.LogicalOperator2_1_6 Bool)
78
(declare-var logic_expand_2_test.LogicalOperator3_1_1 Bool)
79
(declare-var logic_expand_2_test.LogicalOperator3_1_2 Bool)
80
(declare-var logic_expand_2_test.LogicalOperator3_1_3 Bool)
81
(declare-var logic_expand_2_test.LogicalOperator3_1_4 Bool)
82
(declare-var logic_expand_2_test.LogicalOperator3_1_5 Bool)
83
(declare-var logic_expand_2_test.LogicalOperator3_1_6 Bool)
84
(declare-var logic_expand_2_test.LogicalOperator_1_1 Bool)
85
(declare-var logic_expand_2_test.LogicalOperator_1_2 Bool)
86
(declare-var logic_expand_2_test.LogicalOperator_1_3 Bool)
87
(declare-var logic_expand_2_test.LogicalOperator_1_4 Bool)
88
(declare-var logic_expand_2_test.LogicalOperator_1_5 Bool)
89
(declare-var logic_expand_2_test.LogicalOperator_1_6 Bool)
90
(declare-var logic_expand_2_test.__logic_expand_2_test_1 Bool)
91
(declare-var logic_expand_2_test.i_virtual_local Real)
92
(declare-rel logic_expand_2_test_reset (Bool Bool))
93
(declare-rel logic_expand_2_test_step (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
94

    
95
(rule (=> 
96
  (and 
97
       
98
       (= logic_expand_2_test.ni_0._arrow._first_m true)
99
  )
100
  (logic_expand_2_test_reset logic_expand_2_test.ni_0._arrow._first_c
101
                             logic_expand_2_test.ni_0._arrow._first_m)
102
))
103

    
104
(rule (=> 
105
  (and (= logic_expand_2_test.ni_0._arrow._first_m logic_expand_2_test.ni_0._arrow._first_c)
106
       (and (= logic_expand_2_test.__logic_expand_2_test_1 (ite logic_expand_2_test.ni_0._arrow._first_m true false))
107
            (= logic_expand_2_test.ni_0._arrow._first_x false))
108
       (and (or (not (= logic_expand_2_test.__logic_expand_2_test_1 true))
109
               (= logic_expand_2_test.i_virtual_local 0.0))
110
            (or (not (= logic_expand_2_test.__logic_expand_2_test_1 false))
111
               (= logic_expand_2_test.i_virtual_local 1.0))
112
       )
113
       (= logic_expand_2_test.LogicalOperator3_1_6 (and (and logic_expand_2_test.In10_1_6 logic_expand_2_test.In11_1_1) logic_expand_2_test.In12_1_1))
114
       (= logic_expand_2_test.Out4_4_6 logic_expand_2_test.LogicalOperator3_1_6)
115
       (= logic_expand_2_test.LogicalOperator3_1_5 (and (and logic_expand_2_test.In10_1_5 logic_expand_2_test.In11_1_1) logic_expand_2_test.In12_1_1))
116
       (= logic_expand_2_test.Out4_4_5 logic_expand_2_test.LogicalOperator3_1_5)
117
       (= logic_expand_2_test.LogicalOperator3_1_4 (and (and logic_expand_2_test.In10_1_4 logic_expand_2_test.In11_1_1) logic_expand_2_test.In12_1_1))
118
       (= logic_expand_2_test.Out4_4_4 logic_expand_2_test.LogicalOperator3_1_4)
119
       (= logic_expand_2_test.LogicalOperator3_1_3 (and (and logic_expand_2_test.In10_1_3 logic_expand_2_test.In11_1_1) logic_expand_2_test.In12_1_1))
120
       (= logic_expand_2_test.Out4_4_3 logic_expand_2_test.LogicalOperator3_1_3)
121
       (= logic_expand_2_test.LogicalOperator3_1_2 (and (and logic_expand_2_test.In10_1_2 logic_expand_2_test.In11_1_1) logic_expand_2_test.In12_1_1))
122
       (= logic_expand_2_test.Out4_4_2 logic_expand_2_test.LogicalOperator3_1_2)
123
       (= logic_expand_2_test.LogicalOperator3_1_1 (and (and logic_expand_2_test.In10_1_1 logic_expand_2_test.In11_1_1) logic_expand_2_test.In12_1_1))
124
       (= logic_expand_2_test.Out4_4_1 logic_expand_2_test.LogicalOperator3_1_1)
125
       (= logic_expand_2_test.LogicalOperator2_1_6 (and (and logic_expand_2_test.In7_1_1 logic_expand_2_test.In8_1_1) logic_expand_2_test.In9_1_6))
126
       (= logic_expand_2_test.Out3_3_6 logic_expand_2_test.LogicalOperator2_1_6)
127
       (= logic_expand_2_test.LogicalOperator2_1_5 (and (and logic_expand_2_test.In7_1_1 logic_expand_2_test.In8_1_1) logic_expand_2_test.In9_1_5))
128
       (= logic_expand_2_test.Out3_3_5 logic_expand_2_test.LogicalOperator2_1_5)
129
       (= logic_expand_2_test.LogicalOperator2_1_4 (and (and logic_expand_2_test.In7_1_1 logic_expand_2_test.In8_1_1) logic_expand_2_test.In9_1_4))
130
       (= logic_expand_2_test.Out3_3_4 logic_expand_2_test.LogicalOperator2_1_4)
131
       (= logic_expand_2_test.LogicalOperator2_1_3 (and (and logic_expand_2_test.In7_1_1 logic_expand_2_test.In8_1_1) logic_expand_2_test.In9_1_3))
132
       (= logic_expand_2_test.Out3_3_3 logic_expand_2_test.LogicalOperator2_1_3)
133
       (= logic_expand_2_test.LogicalOperator2_1_2 (and (and logic_expand_2_test.In7_1_1 logic_expand_2_test.In8_1_1) logic_expand_2_test.In9_1_2))
134
       (= logic_expand_2_test.Out3_3_2 logic_expand_2_test.LogicalOperator2_1_2)
135
       (= logic_expand_2_test.LogicalOperator2_1_1 (and (and logic_expand_2_test.In7_1_1 logic_expand_2_test.In8_1_1) logic_expand_2_test.In9_1_1))
136
       (= logic_expand_2_test.Out3_3_1 logic_expand_2_test.LogicalOperator2_1_1)
137
       (= logic_expand_2_test.LogicalOperator1_1_6 (and (and logic_expand_2_test.In4_1_6 logic_expand_2_test.In5_1_1) logic_expand_2_test.In6_1_6))
138
       (= logic_expand_2_test.Out2_2_6 logic_expand_2_test.LogicalOperator1_1_6)
139
       (= logic_expand_2_test.LogicalOperator1_1_5 (and (and logic_expand_2_test.In4_1_5 logic_expand_2_test.In5_1_1) logic_expand_2_test.In6_1_5))
140
       (= logic_expand_2_test.Out2_2_5 logic_expand_2_test.LogicalOperator1_1_5)
141
       (= logic_expand_2_test.LogicalOperator1_1_4 (and (and logic_expand_2_test.In4_1_4 logic_expand_2_test.In5_1_1) logic_expand_2_test.In6_1_4))
142
       (= logic_expand_2_test.Out2_2_4 logic_expand_2_test.LogicalOperator1_1_4)
143
       (= logic_expand_2_test.LogicalOperator1_1_3 (and (and logic_expand_2_test.In4_1_3 logic_expand_2_test.In5_1_1) logic_expand_2_test.In6_1_3))
144
       (= logic_expand_2_test.Out2_2_3 logic_expand_2_test.LogicalOperator1_1_3)
145
       (= logic_expand_2_test.LogicalOperator1_1_2 (and (and logic_expand_2_test.In4_1_2 logic_expand_2_test.In5_1_1) logic_expand_2_test.In6_1_2))
146
       (= logic_expand_2_test.Out2_2_2 logic_expand_2_test.LogicalOperator1_1_2)
147
       (= logic_expand_2_test.LogicalOperator1_1_1 (and (and logic_expand_2_test.In4_1_1 logic_expand_2_test.In5_1_1) logic_expand_2_test.In6_1_1))
148
       (= logic_expand_2_test.Out2_2_1 logic_expand_2_test.LogicalOperator1_1_1)
149
       (= logic_expand_2_test.LogicalOperator_1_6 (and (and logic_expand_2_test.In1_1_1 logic_expand_2_test.In2_1_6) logic_expand_2_test.In3_1_1))
150
       (= logic_expand_2_test.Out1_1_6 logic_expand_2_test.LogicalOperator_1_6)
151
       (= logic_expand_2_test.LogicalOperator_1_5 (and (and logic_expand_2_test.In1_1_1 logic_expand_2_test.In2_1_5) logic_expand_2_test.In3_1_1))
152
       (= logic_expand_2_test.Out1_1_5 logic_expand_2_test.LogicalOperator_1_5)
153
       (= logic_expand_2_test.LogicalOperator_1_4 (and (and logic_expand_2_test.In1_1_1 logic_expand_2_test.In2_1_4) logic_expand_2_test.In3_1_1))
154
       (= logic_expand_2_test.Out1_1_4 logic_expand_2_test.LogicalOperator_1_4)
155
       (= logic_expand_2_test.LogicalOperator_1_3 (and (and logic_expand_2_test.In1_1_1 logic_expand_2_test.In2_1_3) logic_expand_2_test.In3_1_1))
156
       (= logic_expand_2_test.Out1_1_3 logic_expand_2_test.LogicalOperator_1_3)
157
       (= logic_expand_2_test.LogicalOperator_1_2 (and (and logic_expand_2_test.In1_1_1 logic_expand_2_test.In2_1_2) logic_expand_2_test.In3_1_1))
158
       (= logic_expand_2_test.Out1_1_2 logic_expand_2_test.LogicalOperator_1_2)
159
       (= logic_expand_2_test.LogicalOperator_1_1 (and (and logic_expand_2_test.In1_1_1 logic_expand_2_test.In2_1_1) logic_expand_2_test.In3_1_1))
160
       (= logic_expand_2_test.Out1_1_1 logic_expand_2_test.LogicalOperator_1_1)
161
       )
162
  (logic_expand_2_test_step logic_expand_2_test.In1_1_1
163
                            logic_expand_2_test.In2_1_1
164
                            logic_expand_2_test.In2_1_2
165
                            logic_expand_2_test.In2_1_3
166
                            logic_expand_2_test.In2_1_4
167
                            logic_expand_2_test.In2_1_5
168
                            logic_expand_2_test.In2_1_6
169
                            logic_expand_2_test.In3_1_1
170
                            logic_expand_2_test.In4_1_1
171
                            logic_expand_2_test.In4_1_2
172
                            logic_expand_2_test.In4_1_3
173
                            logic_expand_2_test.In4_1_4
174
                            logic_expand_2_test.In4_1_5
175
                            logic_expand_2_test.In4_1_6
176
                            logic_expand_2_test.In5_1_1
177
                            logic_expand_2_test.In6_1_1
178
                            logic_expand_2_test.In6_1_2
179
                            logic_expand_2_test.In6_1_3
180
                            logic_expand_2_test.In6_1_4
181
                            logic_expand_2_test.In6_1_5
182
                            logic_expand_2_test.In6_1_6
183
                            logic_expand_2_test.In7_1_1
184
                            logic_expand_2_test.In8_1_1
185
                            logic_expand_2_test.In9_1_1
186
                            logic_expand_2_test.In9_1_2
187
                            logic_expand_2_test.In9_1_3
188
                            logic_expand_2_test.In9_1_4
189
                            logic_expand_2_test.In9_1_5
190
                            logic_expand_2_test.In9_1_6
191
                            logic_expand_2_test.In10_1_1
192
                            logic_expand_2_test.In10_1_2
193
                            logic_expand_2_test.In10_1_3
194
                            logic_expand_2_test.In10_1_4
195
                            logic_expand_2_test.In10_1_5
196
                            logic_expand_2_test.In10_1_6
197
                            logic_expand_2_test.In11_1_1
198
                            logic_expand_2_test.In12_1_1
199
                            logic_expand_2_test.Out1_1_1
200
                            logic_expand_2_test.Out1_1_2
201
                            logic_expand_2_test.Out1_1_3
202
                            logic_expand_2_test.Out1_1_4
203
                            logic_expand_2_test.Out1_1_5
204
                            logic_expand_2_test.Out1_1_6
205
                            logic_expand_2_test.Out2_2_1
206
                            logic_expand_2_test.Out2_2_2
207
                            logic_expand_2_test.Out2_2_3
208
                            logic_expand_2_test.Out2_2_4
209
                            logic_expand_2_test.Out2_2_5
210
                            logic_expand_2_test.Out2_2_6
211
                            logic_expand_2_test.Out3_3_1
212
                            logic_expand_2_test.Out3_3_2
213
                            logic_expand_2_test.Out3_3_3
214
                            logic_expand_2_test.Out3_3_4
215
                            logic_expand_2_test.Out3_3_5
216
                            logic_expand_2_test.Out3_3_6
217
                            logic_expand_2_test.Out4_4_1
218
                            logic_expand_2_test.Out4_4_2
219
                            logic_expand_2_test.Out4_4_3
220
                            logic_expand_2_test.Out4_4_4
221
                            logic_expand_2_test.Out4_4_5
222
                            logic_expand_2_test.Out4_4_6
223
                            logic_expand_2_test.ni_0._arrow._first_c
224
                            logic_expand_2_test.ni_0._arrow._first_x)
225
))
226