Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_memory_test / memory_test.smt2 @ 6c3ea955

History | View | Annotate | Download (9.99 KB)

1
; memory_test
2
(declare-var memory_test.In1_1_1 Real)
3
(declare-var memory_test.In2_1_1 Real)
4
(declare-var memory_test.In3_1_1 Real)
5
(declare-var memory_test.In4_1_1 Int)
6
(declare-var memory_test.In5_1_1 Int)
7
(declare-var memory_test.In6_1_1 Int)
8
(declare-var memory_test.In7_1_1 Bool)
9
(declare-var memory_test.In8_1_1 Bool)
10
(declare-var memory_test.In9_1_1 Bool)
11
(declare-var memory_test.Out1_1_1 Real)
12
(declare-var memory_test.Out2_2_1 Real)
13
(declare-var memory_test.Out3_3_1 Real)
14
(declare-var memory_test.Out4_4_1 Int)
15
(declare-var memory_test.Out5_5_1 Int)
16
(declare-var memory_test.Out6_6_1 Int)
17
(declare-var memory_test.Out7_7_1 Bool)
18
(declare-var memory_test.Out8_8_1 Bool)
19
(declare-var memory_test.Out9_9_1 Bool)
20
(declare-var memory_test.__memory_test_10_c Real)
21
(declare-var memory_test.__memory_test_2_c Bool)
22
(declare-var memory_test.__memory_test_3_c Bool)
23
(declare-var memory_test.__memory_test_4_c Bool)
24
(declare-var memory_test.__memory_test_5_c Int)
25
(declare-var memory_test.__memory_test_6_c Int)
26
(declare-var memory_test.__memory_test_7_c Int)
27
(declare-var memory_test.__memory_test_8_c Real)
28
(declare-var memory_test.__memory_test_9_c Real)
29
(declare-var memory_test.ni_0._arrow._first_c Bool)
30
(declare-var memory_test.__memory_test_10_m Real)
31
(declare-var memory_test.__memory_test_2_m Bool)
32
(declare-var memory_test.__memory_test_3_m Bool)
33
(declare-var memory_test.__memory_test_4_m Bool)
34
(declare-var memory_test.__memory_test_5_m Int)
35
(declare-var memory_test.__memory_test_6_m Int)
36
(declare-var memory_test.__memory_test_7_m Int)
37
(declare-var memory_test.__memory_test_8_m Real)
38
(declare-var memory_test.__memory_test_9_m Real)
39
(declare-var memory_test.ni_0._arrow._first_m Bool)
40
(declare-var memory_test.__memory_test_10_x Real)
41
(declare-var memory_test.__memory_test_2_x Bool)
42
(declare-var memory_test.__memory_test_3_x Bool)
43
(declare-var memory_test.__memory_test_4_x Bool)
44
(declare-var memory_test.__memory_test_5_x Int)
45
(declare-var memory_test.__memory_test_6_x Int)
46
(declare-var memory_test.__memory_test_7_x Int)
47
(declare-var memory_test.__memory_test_8_x Real)
48
(declare-var memory_test.__memory_test_9_x Real)
49
(declare-var memory_test.ni_0._arrow._first_x Bool)
50
(declare-var memory_test.Memory1_1_1 Real)
51
(declare-var memory_test.Memory2_1_1 Real)
52
(declare-var memory_test.Memory3_1_1 Int)
53
(declare-var memory_test.Memory4_1_1 Int)
54
(declare-var memory_test.Memory5_1_1 Int)
55
(declare-var memory_test.Memory6_1_1 Bool)
56
(declare-var memory_test.Memory7_1_1 Bool)
57
(declare-var memory_test.Memory8_1_1 Bool)
58
(declare-var memory_test.Memory_1_1 Real)
59
(declare-var memory_test.__memory_test_1 Bool)
60
(declare-var memory_test.i_virtual_local Real)
61
(declare-rel memory_test_reset (Real Bool Bool Bool Int Int Int Real Real Bool Real Bool Bool Bool Int Int Int Real Real Bool))
62
(declare-rel memory_test_step (Real Real Real Int Int Int Bool Bool Bool Real Real Real Int Int Int Bool Bool Bool Real Bool Bool Bool Int Int Int Real Real Bool Real Bool Bool Bool Int Int Int Real Real Bool))
63

    
64
(rule (=> 
65
  (and 
66
       (= memory_test.__memory_test_10_m memory_test.__memory_test_10_c)
67
       (= memory_test.__memory_test_2_m memory_test.__memory_test_2_c)
68
       (= memory_test.__memory_test_3_m memory_test.__memory_test_3_c)
69
       (= memory_test.__memory_test_4_m memory_test.__memory_test_4_c)
70
       (= memory_test.__memory_test_5_m memory_test.__memory_test_5_c)
71
       (= memory_test.__memory_test_6_m memory_test.__memory_test_6_c)
72
       (= memory_test.__memory_test_7_m memory_test.__memory_test_7_c)
73
       (= memory_test.__memory_test_8_m memory_test.__memory_test_8_c)
74
       (= memory_test.__memory_test_9_m memory_test.__memory_test_9_c)
75
       (= memory_test.ni_0._arrow._first_m true)
76
  )
77
  (memory_test_reset memory_test.__memory_test_10_c
78
                     memory_test.__memory_test_2_c
79
                     memory_test.__memory_test_3_c
80
                     memory_test.__memory_test_4_c
81
                     memory_test.__memory_test_5_c
82
                     memory_test.__memory_test_6_c
83
                     memory_test.__memory_test_7_c
84
                     memory_test.__memory_test_8_c
85
                     memory_test.__memory_test_9_c
86
                     memory_test.ni_0._arrow._first_c
87
                     memory_test.__memory_test_10_m
88
                     memory_test.__memory_test_2_m
89
                     memory_test.__memory_test_3_m
90
                     memory_test.__memory_test_4_m
91
                     memory_test.__memory_test_5_m
92
                     memory_test.__memory_test_6_m
93
                     memory_test.__memory_test_7_m
94
                     memory_test.__memory_test_8_m
95
                     memory_test.__memory_test_9_m
96
                     memory_test.ni_0._arrow._first_m)
97
))
98

    
99
(rule (=> 
100
  (and (= memory_test.ni_0._arrow._first_m memory_test.ni_0._arrow._first_c)
101
       (and (= memory_test.__memory_test_1 (ite memory_test.ni_0._arrow._first_m true false))
102
            (= memory_test.ni_0._arrow._first_x false))
103
       (and (or (not (= memory_test.__memory_test_1 false))
104
               (and (= memory_test.i_virtual_local 1.0)
105
                    (= memory_test.Memory1_1_1 memory_test.__memory_test_9_c)
106
                    ))
107
            (or (not (= memory_test.__memory_test_1 true))
108
               (and (= memory_test.i_virtual_local 0.0)
109
                    (= memory_test.Memory1_1_1 0.00000000)
110
                    ))
111
       )
112
       (= memory_test.__memory_test_9_x memory_test.In2_1_1)
113
       (and (or (not (= memory_test.__memory_test_1 true))
114
               (= memory_test.Memory2_1_1 1.00000000))
115
            (or (not (= memory_test.__memory_test_1 false))
116
               (= memory_test.Memory2_1_1 memory_test.__memory_test_8_c))
117
       )
118
       (= memory_test.__memory_test_8_x memory_test.In3_1_1)
119
       (and (or (not (= memory_test.__memory_test_1 true))
120
               (= memory_test.Memory3_1_1 0))
121
            (or (not (= memory_test.__memory_test_1 false))
122
               (= memory_test.Memory3_1_1 memory_test.__memory_test_7_c))
123
       )
124
       (= memory_test.__memory_test_7_x memory_test.In4_1_1)
125
       (and (or (not (= memory_test.__memory_test_1 true))
126
               (= memory_test.Memory4_1_1 0))
127
            (or (not (= memory_test.__memory_test_1 false))
128
               (= memory_test.Memory4_1_1 memory_test.__memory_test_6_c))
129
       )
130
       (= memory_test.__memory_test_6_x memory_test.In5_1_1)
131
       (and (or (not (= memory_test.__memory_test_1 true))
132
               (= memory_test.Memory5_1_1 1))
133
            (or (not (= memory_test.__memory_test_1 false))
134
               (= memory_test.Memory5_1_1 memory_test.__memory_test_5_c))
135
       )
136
       (= memory_test.__memory_test_5_x memory_test.In6_1_1)
137
       (and (or (not (= memory_test.__memory_test_1 true))
138
               (= memory_test.Memory6_1_1 false))
139
            (or (not (= memory_test.__memory_test_1 false))
140
               (= memory_test.Memory6_1_1 memory_test.__memory_test_4_c))
141
       )
142
       (= memory_test.__memory_test_4_x memory_test.In7_1_1)
143
       (and (or (not (= memory_test.__memory_test_1 true))
144
               (= memory_test.Memory7_1_1 false))
145
            (or (not (= memory_test.__memory_test_1 false))
146
               (= memory_test.Memory7_1_1 memory_test.__memory_test_3_c))
147
       )
148
       (= memory_test.__memory_test_3_x memory_test.In8_1_1)
149
       (and (or (not (= memory_test.__memory_test_1 true))
150
               (= memory_test.Memory8_1_1 true))
151
            (or (not (= memory_test.__memory_test_1 false))
152
               (= memory_test.Memory8_1_1 memory_test.__memory_test_2_c))
153
       )
154
       (= memory_test.__memory_test_2_x memory_test.In9_1_1)
155
       (and (or (not (= memory_test.__memory_test_1 true))
156
               (= memory_test.Memory_1_1 0.00000000))
157
            (or (not (= memory_test.__memory_test_1 false))
158
               (= memory_test.Memory_1_1 memory_test.__memory_test_10_c))
159
       )
160
       (= memory_test.__memory_test_10_x memory_test.In1_1_1)
161
       (= memory_test.Out9_9_1 memory_test.Memory8_1_1)
162
       (= memory_test.Out8_8_1 memory_test.Memory7_1_1)
163
       (= memory_test.Out7_7_1 memory_test.Memory6_1_1)
164
       (= memory_test.Out6_6_1 memory_test.Memory5_1_1)
165
       (= memory_test.Out5_5_1 memory_test.Memory4_1_1)
166
       (= memory_test.Out4_4_1 memory_test.Memory3_1_1)
167
       (= memory_test.Out3_3_1 memory_test.Memory2_1_1)
168
       (= memory_test.Out2_2_1 memory_test.Memory1_1_1)
169
       (= memory_test.Out1_1_1 memory_test.Memory_1_1)
170
       )
171
  (memory_test_step memory_test.In1_1_1
172
                    memory_test.In2_1_1
173
                    memory_test.In3_1_1
174
                    memory_test.In4_1_1
175
                    memory_test.In5_1_1
176
                    memory_test.In6_1_1
177
                    memory_test.In7_1_1
178
                    memory_test.In8_1_1
179
                    memory_test.In9_1_1
180
                    memory_test.Out1_1_1
181
                    memory_test.Out2_2_1
182
                    memory_test.Out3_3_1
183
                    memory_test.Out4_4_1
184
                    memory_test.Out5_5_1
185
                    memory_test.Out6_6_1
186
                    memory_test.Out7_7_1
187
                    memory_test.Out8_8_1
188
                    memory_test.Out9_9_1
189
                    memory_test.__memory_test_10_c
190
                    memory_test.__memory_test_2_c
191
                    memory_test.__memory_test_3_c
192
                    memory_test.__memory_test_4_c
193
                    memory_test.__memory_test_5_c
194
                    memory_test.__memory_test_6_c
195
                    memory_test.__memory_test_7_c
196
                    memory_test.__memory_test_8_c
197
                    memory_test.__memory_test_9_c
198
                    memory_test.ni_0._arrow._first_c
199
                    memory_test.__memory_test_10_x
200
                    memory_test.__memory_test_2_x
201
                    memory_test.__memory_test_3_x
202
                    memory_test.__memory_test_4_x
203
                    memory_test.__memory_test_5_x
204
                    memory_test.__memory_test_6_x
205
                    memory_test.__memory_test_7_x
206
                    memory_test.__memory_test_8_x
207
                    memory_test.__memory_test_9_x
208
                    memory_test.ni_0._arrow._first_x)
209
))
210