Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Stateflow / src_Single1 / Single1.smt2 @ eb639349

History | View | Annotate | Download (38 KB)

1
(declare-datatypes () ((single1_single1__type POINTSingle1_Single1 POINT__TO__SINGLE1_A_1 SINGLE1_A_IDL)));
2

    
3
; Single1_A_en
4
(declare-var Single1_A_en.idSingle1_Single1_1 Int)
5
(declare-var Single1_A_en.isInner Bool)
6
(declare-var Single1_A_en.idSingle1_Single1 Int)
7
(declare-rel Single1_A_en (Int Bool Int))
8
(rule (=> 
9
  (= Single1_A_en.idSingle1_Single1 1790)
10
  (Single1_A_en Single1_A_en.idSingle1_Single1_1 Single1_A_en.isInner Single1_A_en.idSingle1_Single1)
11
))
12

    
13
; Single1_A_du
14
(declare-var Single1_A_du.x_1 Real)
15
(declare-var Single1_A_du.x Real)
16
(declare-rel Single1_A_du (Real Real))
17
(rule (=> 
18
  (= Single1_A_du.x (+ Single1_A_du.x_1 1.))
19
  (Single1_A_du Single1_A_du.x_1 Single1_A_du.x)
20
))
21

    
22
; single1_single1__POINTSingle1_Single1_handler_until
23
(declare-var single1_single1__POINTSingle1_Single1_handler_until.idSingle1_Single1_1 Int)
24
(declare-var single1_single1__POINTSingle1_Single1_handler_until.x_1 Real)
25
(declare-var single1_single1__POINTSingle1_Single1_handler_until.single1_single1__restart_in Bool)
26
(declare-var single1_single1__POINTSingle1_Single1_handler_until.single1_single1__state_in single1_single1__type)
27
(declare-var single1_single1__POINTSingle1_Single1_handler_until.idSingle1_Single1_out Int)
28
(declare-var single1_single1__POINTSingle1_Single1_handler_until.x_out Real)
29
(declare-rel single1_single1__POINTSingle1_Single1_handler_until (Int Real Bool single1_single1__type Int Real))
30
(rule (=> 
31
  (and (= single1_single1__POINTSingle1_Single1_handler_until.x_out single1_single1__POINTSingle1_Single1_handler_until.x_1)
32
       (= single1_single1__POINTSingle1_Single1_handler_until.single1_single1__state_in POINTSingle1_Single1)
33
       (= single1_single1__POINTSingle1_Single1_handler_until.single1_single1__restart_in false)
34
       (= single1_single1__POINTSingle1_Single1_handler_until.idSingle1_Single1_out single1_single1__POINTSingle1_Single1_handler_until.idSingle1_Single1_1)
35
       )
36
  (single1_single1__POINTSingle1_Single1_handler_until single1_single1__POINTSingle1_Single1_handler_until.idSingle1_Single1_1 single1_single1__POINTSingle1_Single1_handler_until.x_1 single1_single1__POINTSingle1_Single1_handler_until.single1_single1__restart_in single1_single1__POINTSingle1_Single1_handler_until.single1_single1__state_in single1_single1__POINTSingle1_Single1_handler_until.idSingle1_Single1_out single1_single1__POINTSingle1_Single1_handler_until.x_out)
37
))
38

    
39
; single1_single1__POINTSingle1_Single1_unless
40
(declare-var single1_single1__POINTSingle1_Single1_unless.single1_single1__restart_in Bool)
41
(declare-var single1_single1__POINTSingle1_Single1_unless.single1_single1__state_in single1_single1__type)
42
(declare-var single1_single1__POINTSingle1_Single1_unless.idSingle1_Single1_1 Int)
43
(declare-var single1_single1__POINTSingle1_Single1_unless.single1_single1__restart_act Bool)
44
(declare-var single1_single1__POINTSingle1_Single1_unless.single1_single1__state_act single1_single1__type)
45
(declare-var single1_single1__POINTSingle1_Single1_unless.__single1_single1__POINTSingle1_Single1_unless_1 Bool)
46
(declare-var single1_single1__POINTSingle1_Single1_unless.__single1_single1__POINTSingle1_Single1_unless_2 Bool)
47
(declare-rel single1_single1__POINTSingle1_Single1_unless (Bool single1_single1__type Int Bool single1_single1__type))
48
(rule (=> 
49
  (and (= single1_single1__POINTSingle1_Single1_unless.__single1_single1__POINTSingle1_Single1_unless_2 (= single1_single1__POINTSingle1_Single1_unless.idSingle1_Single1_1 1790))
50
       (= single1_single1__POINTSingle1_Single1_unless.__single1_single1__POINTSingle1_Single1_unless_1 (= single1_single1__POINTSingle1_Single1_unless.idSingle1_Single1_1 0))
51
       (and (or (not (= single1_single1__POINTSingle1_Single1_unless.__single1_single1__POINTSingle1_Single1_unless_1 false))
52
               (and (or (not (= single1_single1__POINTSingle1_Single1_unless.__single1_single1__POINTSingle1_Single1_unless_2 false))
53
                       (and (= single1_single1__POINTSingle1_Single1_unless.single1_single1__state_act single1_single1__POINTSingle1_Single1_unless.single1_single1__state_in)
54
                            (= single1_single1__POINTSingle1_Single1_unless.single1_single1__restart_act single1_single1__POINTSingle1_Single1_unless.single1_single1__restart_in)
55
                            ))
56
                    (or (not (= single1_single1__POINTSingle1_Single1_unless.__single1_single1__POINTSingle1_Single1_unless_2 true))
57
                       (and (= single1_single1__POINTSingle1_Single1_unless.single1_single1__state_act SINGLE1_A_IDL)
58
                            (= single1_single1__POINTSingle1_Single1_unless.single1_single1__restart_act true)
59
                            ))
60
               ))
61
            (or (not (= single1_single1__POINTSingle1_Single1_unless.__single1_single1__POINTSingle1_Single1_unless_1 true))
62
               (and (= single1_single1__POINTSingle1_Single1_unless.single1_single1__state_act POINT__TO__SINGLE1_A_1)
63
                    (= single1_single1__POINTSingle1_Single1_unless.single1_single1__restart_act true)
64
                    ))
65
       )
66
       )
67
  (single1_single1__POINTSingle1_Single1_unless single1_single1__POINTSingle1_Single1_unless.single1_single1__restart_in single1_single1__POINTSingle1_Single1_unless.single1_single1__state_in single1_single1__POINTSingle1_Single1_unless.idSingle1_Single1_1 single1_single1__POINTSingle1_Single1_unless.single1_single1__restart_act single1_single1__POINTSingle1_Single1_unless.single1_single1__state_act)
68
))
69

    
70
; single1_single1__POINT__TO__SINGLE1_A_1_handler_until
71
(declare-var single1_single1__POINT__TO__SINGLE1_A_1_handler_until.idSingle1_Single1_1 Int)
72
(declare-var single1_single1__POINT__TO__SINGLE1_A_1_handler_until.x_1 Real)
73
(declare-var single1_single1__POINT__TO__SINGLE1_A_1_handler_until.single1_single1__restart_in Bool)
74
(declare-var single1_single1__POINT__TO__SINGLE1_A_1_handler_until.single1_single1__state_in single1_single1__type)
75
(declare-var single1_single1__POINT__TO__SINGLE1_A_1_handler_until.idSingle1_Single1_out Int)
76
(declare-var single1_single1__POINT__TO__SINGLE1_A_1_handler_until.x_out Real)
77
(declare-var single1_single1__POINT__TO__SINGLE1_A_1_handler_until.idSingle1_Single1_2 Int)
78
(declare-rel single1_single1__POINT__TO__SINGLE1_A_1_handler_until (Int Real Bool single1_single1__type Int Real))
79
(rule (=> 
80
  (and (= single1_single1__POINT__TO__SINGLE1_A_1_handler_until.x_out single1_single1__POINT__TO__SINGLE1_A_1_handler_until.x_1)
81
       (= single1_single1__POINT__TO__SINGLE1_A_1_handler_until.single1_single1__state_in POINTSingle1_Single1)
82
       (= single1_single1__POINT__TO__SINGLE1_A_1_handler_until.single1_single1__restart_in true)
83
       (Single1_A_en single1_single1__POINT__TO__SINGLE1_A_1_handler_until.idSingle1_Single1_1
84
                     false
85
                     single1_single1__POINT__TO__SINGLE1_A_1_handler_until.idSingle1_Single1_2)
86
       (= single1_single1__POINT__TO__SINGLE1_A_1_handler_until.idSingle1_Single1_out single1_single1__POINT__TO__SINGLE1_A_1_handler_until.idSingle1_Single1_2)
87
       )
88
  (single1_single1__POINT__TO__SINGLE1_A_1_handler_until single1_single1__POINT__TO__SINGLE1_A_1_handler_until.idSingle1_Single1_1 single1_single1__POINT__TO__SINGLE1_A_1_handler_until.x_1 single1_single1__POINT__TO__SINGLE1_A_1_handler_until.single1_single1__restart_in single1_single1__POINT__TO__SINGLE1_A_1_handler_until.single1_single1__state_in single1_single1__POINT__TO__SINGLE1_A_1_handler_until.idSingle1_Single1_out single1_single1__POINT__TO__SINGLE1_A_1_handler_until.x_out)
89
))
90

    
91
; single1_single1__POINT__TO__SINGLE1_A_1_unless
92
(declare-var single1_single1__POINT__TO__SINGLE1_A_1_unless.single1_single1__restart_in Bool)
93
(declare-var single1_single1__POINT__TO__SINGLE1_A_1_unless.single1_single1__state_in single1_single1__type)
94
(declare-var single1_single1__POINT__TO__SINGLE1_A_1_unless.single1_single1__restart_act Bool)
95
(declare-var single1_single1__POINT__TO__SINGLE1_A_1_unless.single1_single1__state_act single1_single1__type)
96
(declare-rel single1_single1__POINT__TO__SINGLE1_A_1_unless (Bool single1_single1__type Bool single1_single1__type))
97
(rule (=> 
98
  (and (= single1_single1__POINT__TO__SINGLE1_A_1_unless.single1_single1__state_act single1_single1__POINT__TO__SINGLE1_A_1_unless.single1_single1__state_in)
99
       (= single1_single1__POINT__TO__SINGLE1_A_1_unless.single1_single1__restart_act single1_single1__POINT__TO__SINGLE1_A_1_unless.single1_single1__restart_in)
100
       )
101
  (single1_single1__POINT__TO__SINGLE1_A_1_unless single1_single1__POINT__TO__SINGLE1_A_1_unless.single1_single1__restart_in single1_single1__POINT__TO__SINGLE1_A_1_unless.single1_single1__state_in single1_single1__POINT__TO__SINGLE1_A_1_unless.single1_single1__restart_act single1_single1__POINT__TO__SINGLE1_A_1_unless.single1_single1__state_act)
102
))
103

    
104
; single1_single1__SINGLE1_A_IDL_handler_until
105
(declare-var single1_single1__SINGLE1_A_IDL_handler_until.idSingle1_Single1_1 Int)
106
(declare-var single1_single1__SINGLE1_A_IDL_handler_until.x_1 Real)
107
(declare-var single1_single1__SINGLE1_A_IDL_handler_until.single1_single1__restart_in Bool)
108
(declare-var single1_single1__SINGLE1_A_IDL_handler_until.single1_single1__state_in single1_single1__type)
109
(declare-var single1_single1__SINGLE1_A_IDL_handler_until.idSingle1_Single1_out Int)
110
(declare-var single1_single1__SINGLE1_A_IDL_handler_until.x_out Real)
111
(declare-var single1_single1__SINGLE1_A_IDL_handler_until.x_2 Real)
112
(declare-rel single1_single1__SINGLE1_A_IDL_handler_until (Int Real Bool single1_single1__type Int Real))
113
(rule (=> 
114
  (and (Single1_A_du single1_single1__SINGLE1_A_IDL_handler_until.x_1
115
                     single1_single1__SINGLE1_A_IDL_handler_until.x_2)
116
       (= single1_single1__SINGLE1_A_IDL_handler_until.x_out single1_single1__SINGLE1_A_IDL_handler_until.x_2)
117
       (= single1_single1__SINGLE1_A_IDL_handler_until.single1_single1__state_in POINTSingle1_Single1)
118
       (= single1_single1__SINGLE1_A_IDL_handler_until.single1_single1__restart_in true)
119
       (= single1_single1__SINGLE1_A_IDL_handler_until.idSingle1_Single1_out single1_single1__SINGLE1_A_IDL_handler_until.idSingle1_Single1_1)
120
       )
121
  (single1_single1__SINGLE1_A_IDL_handler_until single1_single1__SINGLE1_A_IDL_handler_until.idSingle1_Single1_1 single1_single1__SINGLE1_A_IDL_handler_until.x_1 single1_single1__SINGLE1_A_IDL_handler_until.single1_single1__restart_in single1_single1__SINGLE1_A_IDL_handler_until.single1_single1__state_in single1_single1__SINGLE1_A_IDL_handler_until.idSingle1_Single1_out single1_single1__SINGLE1_A_IDL_handler_until.x_out)
122
))
123

    
124
; single1_single1__SINGLE1_A_IDL_unless
125
(declare-var single1_single1__SINGLE1_A_IDL_unless.single1_single1__restart_in Bool)
126
(declare-var single1_single1__SINGLE1_A_IDL_unless.single1_single1__state_in single1_single1__type)
127
(declare-var single1_single1__SINGLE1_A_IDL_unless.single1_single1__restart_act Bool)
128
(declare-var single1_single1__SINGLE1_A_IDL_unless.single1_single1__state_act single1_single1__type)
129
(declare-rel single1_single1__SINGLE1_A_IDL_unless (Bool single1_single1__type Bool single1_single1__type))
130
(rule (=> 
131
  (and (= single1_single1__SINGLE1_A_IDL_unless.single1_single1__state_act single1_single1__SINGLE1_A_IDL_unless.single1_single1__state_in)
132
       (= single1_single1__SINGLE1_A_IDL_unless.single1_single1__restart_act single1_single1__SINGLE1_A_IDL_unless.single1_single1__restart_in)
133
       )
134
  (single1_single1__SINGLE1_A_IDL_unless single1_single1__SINGLE1_A_IDL_unless.single1_single1__restart_in single1_single1__SINGLE1_A_IDL_unless.single1_single1__state_in single1_single1__SINGLE1_A_IDL_unless.single1_single1__restart_act single1_single1__SINGLE1_A_IDL_unless.single1_single1__state_act)
135
))
136

    
137
; Single1_Single1_node
138
(declare-var Single1_Single1_node.idSingle1_Single1_1 Int)
139
(declare-var Single1_Single1_node.x_1 Real)
140
(declare-var Single1_Single1_node.idSingle1_Single1 Int)
141
(declare-var Single1_Single1_node.x Real)
142
(declare-var Single1_Single1_node.__Single1_Single1_node_20_c Bool)
143
(declare-var Single1_Single1_node.__Single1_Single1_node_21_c single1_single1__type)
144
(declare-var Single1_Single1_node.ni_4._arrow._first_c Bool)
145
(declare-var Single1_Single1_node.__Single1_Single1_node_20_m Bool)
146
(declare-var Single1_Single1_node.__Single1_Single1_node_21_m single1_single1__type)
147
(declare-var Single1_Single1_node.ni_4._arrow._first_m Bool)
148
(declare-var Single1_Single1_node.__Single1_Single1_node_20_x Bool)
149
(declare-var Single1_Single1_node.__Single1_Single1_node_21_x single1_single1__type)
150
(declare-var Single1_Single1_node.ni_4._arrow._first_x Bool)
151
(declare-var Single1_Single1_node.__Single1_Single1_node_1 Bool)
152
(declare-var Single1_Single1_node.__Single1_Single1_node_10 Real)
153
(declare-var Single1_Single1_node.__Single1_Single1_node_11 Bool)
154
(declare-var Single1_Single1_node.__Single1_Single1_node_12 single1_single1__type)
155
(declare-var Single1_Single1_node.__Single1_Single1_node_13 Int)
156
(declare-var Single1_Single1_node.__Single1_Single1_node_14 Real)
157
(declare-var Single1_Single1_node.__Single1_Single1_node_15 Bool)
158
(declare-var Single1_Single1_node.__Single1_Single1_node_16 single1_single1__type)
159
(declare-var Single1_Single1_node.__Single1_Single1_node_17 Int)
160
(declare-var Single1_Single1_node.__Single1_Single1_node_18 Real)
161
(declare-var Single1_Single1_node.__Single1_Single1_node_19 Bool)
162
(declare-var Single1_Single1_node.__Single1_Single1_node_2 single1_single1__type)
163
(declare-var Single1_Single1_node.__Single1_Single1_node_3 Bool)
164
(declare-var Single1_Single1_node.__Single1_Single1_node_4 single1_single1__type)
165
(declare-var Single1_Single1_node.__Single1_Single1_node_5 Bool)
166
(declare-var Single1_Single1_node.__Single1_Single1_node_6 single1_single1__type)
167
(declare-var Single1_Single1_node.__Single1_Single1_node_7 Bool)
168
(declare-var Single1_Single1_node.__Single1_Single1_node_8 single1_single1__type)
169
(declare-var Single1_Single1_node.__Single1_Single1_node_9 Int)
170
(declare-var Single1_Single1_node.single1_single1__next_restart_in Bool)
171
(declare-var Single1_Single1_node.single1_single1__next_state_in single1_single1__type)
172
(declare-var Single1_Single1_node.single1_single1__restart_act Bool)
173
(declare-var Single1_Single1_node.single1_single1__restart_in Bool)
174
(declare-var Single1_Single1_node.single1_single1__state_act single1_single1__type)
175
(declare-var Single1_Single1_node.single1_single1__state_in single1_single1__type)
176
(declare-rel Single1_Single1_node_reset (Bool single1_single1__type Bool Bool single1_single1__type Bool))
177
(declare-rel Single1_Single1_node_step (Int Real Int Real Bool single1_single1__type Bool Bool single1_single1__type Bool))
178

    
179
(rule (=> 
180
  (and 
181
       (= Single1_Single1_node.__Single1_Single1_node_20_m Single1_Single1_node.__Single1_Single1_node_20_c)
182
       (= Single1_Single1_node.__Single1_Single1_node_21_m Single1_Single1_node.__Single1_Single1_node_21_c)
183
       (= Single1_Single1_node.ni_4._arrow._first_m true)
184
  )
185
  (Single1_Single1_node_reset Single1_Single1_node.__Single1_Single1_node_20_c
186
                              Single1_Single1_node.__Single1_Single1_node_21_c
187
                              Single1_Single1_node.ni_4._arrow._first_c
188
                              Single1_Single1_node.__Single1_Single1_node_20_m
189
                              Single1_Single1_node.__Single1_Single1_node_21_m
190
                              Single1_Single1_node.ni_4._arrow._first_m)
191
))
192

    
193
(rule (=> 
194
  (and (= Single1_Single1_node.ni_4._arrow._first_m Single1_Single1_node.ni_4._arrow._first_c)
195
       (and (= Single1_Single1_node.__Single1_Single1_node_19 (ite Single1_Single1_node.ni_4._arrow._first_m true false))
196
            (= Single1_Single1_node.ni_4._arrow._first_x false))
197
       (and (or (not (= Single1_Single1_node.__Single1_Single1_node_19 false))
198
               (and (= Single1_Single1_node.single1_single1__state_in Single1_Single1_node.__Single1_Single1_node_21_c)
199
                    (= Single1_Single1_node.single1_single1__restart_in Single1_Single1_node.__Single1_Single1_node_20_c)
200
                    ))
201
            (or (not (= Single1_Single1_node.__Single1_Single1_node_19 true))
202
               (and (= Single1_Single1_node.single1_single1__state_in POINTSingle1_Single1)
203
                    (= Single1_Single1_node.single1_single1__restart_in false)
204
                    ))
205
       )
206
       (and (or (not (= Single1_Single1_node.single1_single1__state_in POINTSingle1_Single1))
207
               (and (single1_single1__POINTSingle1_Single1_unless Single1_Single1_node.single1_single1__restart_in
208
                                                                  Single1_Single1_node.single1_single1__state_in
209
                                                                  Single1_Single1_node.idSingle1_Single1_1
210
                                                                  Single1_Single1_node.__Single1_Single1_node_5
211
                                                                  Single1_Single1_node.__Single1_Single1_node_6)
212
                    (= Single1_Single1_node.single1_single1__state_act Single1_Single1_node.__Single1_Single1_node_6)
213
                    (= Single1_Single1_node.single1_single1__restart_act Single1_Single1_node.__Single1_Single1_node_5)
214
                    ))
215
            (or (not (= Single1_Single1_node.single1_single1__state_in POINT__TO__SINGLE1_A_1))
216
               (and (single1_single1__POINT__TO__SINGLE1_A_1_unless Single1_Single1_node.single1_single1__restart_in
217
                                                                    Single1_Single1_node.single1_single1__state_in
218
                                                                    Single1_Single1_node.__Single1_Single1_node_3
219
                                                                    Single1_Single1_node.__Single1_Single1_node_4)
220
                    (= Single1_Single1_node.single1_single1__state_act Single1_Single1_node.__Single1_Single1_node_4)
221
                    (= Single1_Single1_node.single1_single1__restart_act Single1_Single1_node.__Single1_Single1_node_3)
222
                    ))
223
            (or (not (= Single1_Single1_node.single1_single1__state_in SINGLE1_A_IDL))
224
               (and (single1_single1__SINGLE1_A_IDL_unless Single1_Single1_node.single1_single1__restart_in
225
                                                           Single1_Single1_node.single1_single1__state_in
226
                                                           Single1_Single1_node.__Single1_Single1_node_1
227
                                                           Single1_Single1_node.__Single1_Single1_node_2)
228
                    (= Single1_Single1_node.single1_single1__state_act Single1_Single1_node.__Single1_Single1_node_2)
229
                    (= Single1_Single1_node.single1_single1__restart_act Single1_Single1_node.__Single1_Single1_node_1)
230
                    ))
231
       )
232
       (and (or (not (= Single1_Single1_node.single1_single1__state_act POINTSingle1_Single1))
233
               (and (single1_single1__POINTSingle1_Single1_handler_until 
234
                    Single1_Single1_node.idSingle1_Single1_1
235
                    Single1_Single1_node.x_1
236
                    Single1_Single1_node.__Single1_Single1_node_15
237
                    Single1_Single1_node.__Single1_Single1_node_16
238
                    Single1_Single1_node.__Single1_Single1_node_17
239
                    Single1_Single1_node.__Single1_Single1_node_18)
240
                    (= Single1_Single1_node.x Single1_Single1_node.__Single1_Single1_node_18)
241
                    (= Single1_Single1_node.single1_single1__next_state_in Single1_Single1_node.__Single1_Single1_node_16)
242
                    (= Single1_Single1_node.single1_single1__next_restart_in Single1_Single1_node.__Single1_Single1_node_15)
243
                    (= Single1_Single1_node.idSingle1_Single1 Single1_Single1_node.__Single1_Single1_node_17)
244
                    ))
245
            (or (not (= Single1_Single1_node.single1_single1__state_act POINT__TO__SINGLE1_A_1))
246
               (and (single1_single1__POINT__TO__SINGLE1_A_1_handler_until 
247
                    Single1_Single1_node.idSingle1_Single1_1
248
                    Single1_Single1_node.x_1
249
                    Single1_Single1_node.__Single1_Single1_node_11
250
                    Single1_Single1_node.__Single1_Single1_node_12
251
                    Single1_Single1_node.__Single1_Single1_node_13
252
                    Single1_Single1_node.__Single1_Single1_node_14)
253
                    (= Single1_Single1_node.x Single1_Single1_node.__Single1_Single1_node_14)
254
                    (= Single1_Single1_node.single1_single1__next_state_in Single1_Single1_node.__Single1_Single1_node_12)
255
                    (= Single1_Single1_node.single1_single1__next_restart_in Single1_Single1_node.__Single1_Single1_node_11)
256
                    (= Single1_Single1_node.idSingle1_Single1 Single1_Single1_node.__Single1_Single1_node_13)
257
                    ))
258
            (or (not (= Single1_Single1_node.single1_single1__state_act SINGLE1_A_IDL))
259
               (and (single1_single1__SINGLE1_A_IDL_handler_until Single1_Single1_node.idSingle1_Single1_1
260
                                                                  Single1_Single1_node.x_1
261
                                                                  Single1_Single1_node.__Single1_Single1_node_7
262
                                                                  Single1_Single1_node.__Single1_Single1_node_8
263
                                                                  Single1_Single1_node.__Single1_Single1_node_9
264
                                                                  Single1_Single1_node.__Single1_Single1_node_10)
265
                    (= Single1_Single1_node.x Single1_Single1_node.__Single1_Single1_node_10)
266
                    (= Single1_Single1_node.single1_single1__next_state_in Single1_Single1_node.__Single1_Single1_node_8)
267
                    (= Single1_Single1_node.single1_single1__next_restart_in Single1_Single1_node.__Single1_Single1_node_7)
268
                    (= Single1_Single1_node.idSingle1_Single1 Single1_Single1_node.__Single1_Single1_node_9)
269
                    ))
270
       )
271
       (= Single1_Single1_node.__Single1_Single1_node_21_x Single1_Single1_node.single1_single1__next_state_in)
272
       (= Single1_Single1_node.__Single1_Single1_node_20_x Single1_Single1_node.single1_single1__next_restart_in)
273
       )
274
  (Single1_Single1_node_step Single1_Single1_node.idSingle1_Single1_1
275
                             Single1_Single1_node.x_1
276
                             Single1_Single1_node.idSingle1_Single1
277
                             Single1_Single1_node.x
278
                             Single1_Single1_node.__Single1_Single1_node_20_c
279
                             Single1_Single1_node.__Single1_Single1_node_21_c
280
                             Single1_Single1_node.ni_4._arrow._first_c
281
                             Single1_Single1_node.__Single1_Single1_node_20_x
282
                             Single1_Single1_node.__Single1_Single1_node_21_x
283
                             Single1_Single1_node.ni_4._arrow._first_x)
284
))
285

    
286
; Single1_Single1
287
(declare-var Single1_Single1.noInput Bool)
288
(declare-var Single1_Single1.x Real)
289
(declare-var Single1_Single1.__Single1_Single1_2_c Int)
290
(declare-var Single1_Single1.__Single1_Single1_3_c Real)
291
(declare-var Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_c Bool)
292
(declare-var Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_c single1_single1__type)
293
(declare-var Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_c Bool)
294
(declare-var Single1_Single1.ni_3._arrow._first_c Bool)
295
(declare-var Single1_Single1.__Single1_Single1_2_m Int)
296
(declare-var Single1_Single1.__Single1_Single1_3_m Real)
297
(declare-var Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_m Bool)
298
(declare-var Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_m single1_single1__type)
299
(declare-var Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_m Bool)
300
(declare-var Single1_Single1.ni_3._arrow._first_m Bool)
301
(declare-var Single1_Single1.__Single1_Single1_2_x Int)
302
(declare-var Single1_Single1.__Single1_Single1_3_x Real)
303
(declare-var Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_x Bool)
304
(declare-var Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_x single1_single1__type)
305
(declare-var Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_x Bool)
306
(declare-var Single1_Single1.ni_3._arrow._first_x Bool)
307
(declare-var Single1_Single1.__Single1_Single1_1 Bool)
308
(declare-var Single1_Single1.idSingle1_Single1 Int)
309
(declare-var Single1_Single1.idSingle1_Single1_1 Int)
310
(declare-var Single1_Single1.x_1 Real)
311
(declare-rel Single1_Single1_reset (Int Real Bool single1_single1__type Bool Bool Int Real Bool single1_single1__type Bool Bool))
312
(declare-rel Single1_Single1_step (Bool Real Int Real Bool single1_single1__type Bool Bool Int Real Bool single1_single1__type Bool Bool))
313

    
314
(rule (=> 
315
  (and 
316
       (= Single1_Single1.__Single1_Single1_2_m Single1_Single1.__Single1_Single1_2_c)
317
       (= Single1_Single1.__Single1_Single1_3_m Single1_Single1.__Single1_Single1_3_c)
318
       (= Single1_Single1.ni_3._arrow._first_m true)
319
       (Single1_Single1_node_reset Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_c
320
                                   Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_c
321
                                   Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_c
322
                                   Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_m
323
                                   Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_m
324
                                   Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_m)
325
  )
326
  (Single1_Single1_reset Single1_Single1.__Single1_Single1_2_c
327
                         Single1_Single1.__Single1_Single1_3_c
328
                         Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_c
329
                         Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_c
330
                         Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_c
331
                         Single1_Single1.ni_3._arrow._first_c
332
                         Single1_Single1.__Single1_Single1_2_m
333
                         Single1_Single1.__Single1_Single1_3_m
334
                         Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_m
335
                         Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_m
336
                         Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_m
337
                         Single1_Single1.ni_3._arrow._first_m)
338
))
339

    
340
(rule (=> 
341
  (and (= Single1_Single1.ni_3._arrow._first_m Single1_Single1.ni_3._arrow._first_c)
342
       (and (= Single1_Single1.__Single1_Single1_1 (ite Single1_Single1.ni_3._arrow._first_m true false))
343
            (= Single1_Single1.ni_3._arrow._first_x false))
344
       (and (or (not (= Single1_Single1.__Single1_Single1_1 false))
345
               (and (= Single1_Single1.x_1 Single1_Single1.__Single1_Single1_3_c)
346
                    (= Single1_Single1.idSingle1_Single1_1 Single1_Single1.__Single1_Single1_2_c)
347
                    ))
348
            (or (not (= Single1_Single1.__Single1_Single1_1 true))
349
               (and (= Single1_Single1.x_1 0.)
350
                    (= Single1_Single1.idSingle1_Single1_1 0)
351
                    ))
352
       )
353
       (and (= Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_m Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_c)
354
            (= Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_m Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_c)
355
            (= Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_m Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_c)
356
            )
357
       (Single1_Single1_node_step Single1_Single1.idSingle1_Single1_1
358
                                  Single1_Single1.x_1
359
                                  Single1_Single1.idSingle1_Single1
360
                                  Single1_Single1.x
361
                                  Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_m
362
                                  Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_m
363
                                  Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_m
364
                                  Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_x
365
                                  Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_x
366
                                  Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_x)
367
       (= Single1_Single1.__Single1_Single1_3_x Single1_Single1.x)
368
       (= Single1_Single1.__Single1_Single1_2_x Single1_Single1.idSingle1_Single1)
369
       )
370
  (Single1_Single1_step Single1_Single1.noInput
371
                        Single1_Single1.x
372
                        Single1_Single1.__Single1_Single1_2_c
373
                        Single1_Single1.__Single1_Single1_3_c
374
                        Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_c
375
                        Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_c
376
                        Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_c
377
                        Single1_Single1.ni_3._arrow._first_c
378
                        Single1_Single1.__Single1_Single1_2_x
379
                        Single1_Single1.__Single1_Single1_3_x
380
                        Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_x
381
                        Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_x
382
                        Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_x
383
                        Single1_Single1.ni_3._arrow._first_x)
384
))
385

    
386
; Single1_A_ex
387
(declare-var Single1_A_ex.idSingle1_Single1_1 Int)
388
(declare-var Single1_A_ex.isInner Bool)
389
(declare-var Single1_A_ex.idSingle1_Single1 Int)
390
(declare-var Single1_A_ex.idSingle1_Single1_2 Int)
391
(declare-rel Single1_A_ex (Int Bool Int))
392
(rule (=> 
393
  (and (and (or (not (= (not Single1_A_ex.isInner) true))
394
               (= Single1_A_ex.idSingle1_Single1_2 0))
395
            (or (not (= (not Single1_A_ex.isInner) false))
396
               (= Single1_A_ex.idSingle1_Single1_2 Single1_A_ex.idSingle1_Single1_1))
397
       )
398
       (= Single1_A_ex.idSingle1_Single1 Single1_A_ex.idSingle1_Single1_1)
399
       )
400
  (Single1_A_ex Single1_A_ex.idSingle1_Single1_1 Single1_A_ex.isInner Single1_A_ex.idSingle1_Single1)
401
))
402

    
403
; Single1
404
(declare-var Single1.i_virtual Real)
405
(declare-var Single1.x_1_1 Real)
406
(declare-var Single1.ni_0._arrow._first_c Bool)
407
(declare-var Single1.ni_1.Single1_Single1.__Single1_Single1_2_c Int)
408
(declare-var Single1.ni_1.Single1_Single1.__Single1_Single1_3_c Real)
409
(declare-var Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_c Bool)
410
(declare-var Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_c single1_single1__type)
411
(declare-var Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_c Bool)
412
(declare-var Single1.ni_1.Single1_Single1.ni_3._arrow._first_c Bool)
413
(declare-var Single1.ni_0._arrow._first_m Bool)
414
(declare-var Single1.ni_1.Single1_Single1.__Single1_Single1_2_m Int)
415
(declare-var Single1.ni_1.Single1_Single1.__Single1_Single1_3_m Real)
416
(declare-var Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_m Bool)
417
(declare-var Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_m single1_single1__type)
418
(declare-var Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_m Bool)
419
(declare-var Single1.ni_1.Single1_Single1.ni_3._arrow._first_m Bool)
420
(declare-var Single1.ni_0._arrow._first_x Bool)
421
(declare-var Single1.ni_1.Single1_Single1.__Single1_Single1_2_x Int)
422
(declare-var Single1.ni_1.Single1_Single1.__Single1_Single1_3_x Real)
423
(declare-var Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_x Bool)
424
(declare-var Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_x single1_single1__type)
425
(declare-var Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_x Bool)
426
(declare-var Single1.ni_1.Single1_Single1.ni_3._arrow._first_x Bool)
427
(declare-var Single1.Single1_1_1 Real)
428
(declare-var Single1.__Single1_1 Bool)
429
(declare-var Single1.i_virtual_local Real)
430
(declare-rel Single1_reset (Bool Int Real Bool single1_single1__type Bool Bool Bool Int Real Bool single1_single1__type Bool Bool))
431
(declare-rel Single1_step (Real Real Bool Int Real Bool single1_single1__type Bool Bool Bool Int Real Bool single1_single1__type Bool Bool))
432

    
433
(rule (=> 
434
  (and 
435
       
436
       (Single1_Single1_reset Single1.ni_1.Single1_Single1.__Single1_Single1_2_c
437
                              Single1.ni_1.Single1_Single1.__Single1_Single1_3_c
438
                              Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_c
439
                              Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_c
440
                              Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_c
441
                              Single1.ni_1.Single1_Single1.ni_3._arrow._first_c
442
                              Single1.ni_1.Single1_Single1.__Single1_Single1_2_m
443
                              Single1.ni_1.Single1_Single1.__Single1_Single1_3_m
444
                              Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_m
445
                              Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_m
446
                              Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_m
447
                              Single1.ni_1.Single1_Single1.ni_3._arrow._first_m)
448
       (= Single1.ni_0._arrow._first_m true)
449
  )
450
  (Single1_reset Single1.ni_0._arrow._first_c
451
                 Single1.ni_1.Single1_Single1.__Single1_Single1_2_c
452
                 Single1.ni_1.Single1_Single1.__Single1_Single1_3_c
453
                 Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_c
454
                 Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_c
455
                 Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_c
456
                 Single1.ni_1.Single1_Single1.ni_3._arrow._first_c
457
                 Single1.ni_0._arrow._first_m
458
                 Single1.ni_1.Single1_Single1.__Single1_Single1_2_m
459
                 Single1.ni_1.Single1_Single1.__Single1_Single1_3_m
460
                 Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_m
461
                 Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_m
462
                 Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_m
463
                 Single1.ni_1.Single1_Single1.ni_3._arrow._first_m)
464
))
465

    
466
(rule (=> 
467
  (and (and (= Single1.ni_1.Single1_Single1.__Single1_Single1_2_m Single1.ni_1.Single1_Single1.__Single1_Single1_2_c)
468
            (= Single1.ni_1.Single1_Single1.__Single1_Single1_3_m Single1.ni_1.Single1_Single1.__Single1_Single1_3_c)
469
            (= Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_m Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_c)
470
            (= Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_m Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_c)
471
            (= Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_m Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_c)
472
            (= Single1.ni_1.Single1_Single1.ni_3._arrow._first_m Single1.ni_1.Single1_Single1.ni_3._arrow._first_c)
473
            )
474
       (Single1_Single1_step true
475
                             Single1.Single1_1_1
476
                             Single1.ni_1.Single1_Single1.__Single1_Single1_2_m
477
                             Single1.ni_1.Single1_Single1.__Single1_Single1_3_m
478
                             Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_m
479
                             Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_m
480
                             Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_m
481
                             Single1.ni_1.Single1_Single1.ni_3._arrow._first_m
482
                             Single1.ni_1.Single1_Single1.__Single1_Single1_2_x
483
                             Single1.ni_1.Single1_Single1.__Single1_Single1_3_x
484
                             Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_x
485
                             Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_x
486
                             Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_x
487
                             Single1.ni_1.Single1_Single1.ni_3._arrow._first_x)
488
       (= Single1.x_1_1 Single1.Single1_1_1)
489
       (= Single1.ni_0._arrow._first_m Single1.ni_0._arrow._first_c)(and (= Single1.__Single1_1 (ite Single1.ni_0._arrow._first_m true false))
490
                                                                    (= Single1.ni_0._arrow._first_x false))
491
       (and (or (not (= Single1.__Single1_1 true))
492
               (= Single1.i_virtual_local 0.))
493
            (or (not (= Single1.__Single1_1 false))
494
               (= Single1.i_virtual_local 1.))
495
       )
496
       )
497
  (Single1_step Single1.i_virtual
498
                Single1.x_1_1
499
                Single1.ni_0._arrow._first_c
500
                Single1.ni_1.Single1_Single1.__Single1_Single1_2_c
501
                Single1.ni_1.Single1_Single1.__Single1_Single1_3_c
502
                Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_c
503
                Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_c
504
                Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_c
505
                Single1.ni_1.Single1_Single1.ni_3._arrow._first_c
506
                Single1.ni_0._arrow._first_x
507
                Single1.ni_1.Single1_Single1.__Single1_Single1_2_x
508
                Single1.ni_1.Single1_Single1.__Single1_Single1_3_x
509
                Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_20_x
510
                Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.__Single1_Single1_node_21_x
511
                Single1.ni_1.Single1_Single1.ni_2.Single1_Single1_node.ni_4._arrow._first_x
512
                Single1.ni_1.Single1_Single1.ni_3._arrow._first_x)
513
))
514