Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_sum_collapse_int_test / sum_collapse_int_test.smt2 @ 6c3ea955

History | View | Annotate | Download (9.9 KB)

1
; sum_collapse_int_test
2
(declare-var sum_collapse_int_test.In9_1_1 Int)
3
(declare-var sum_collapse_int_test.In10_1_1 Int)
4
(declare-var sum_collapse_int_test.In11_1_1 Int)
5
(declare-var sum_collapse_int_test.In11_1_2 Int)
6
(declare-var sum_collapse_int_test.In11_1_3 Int)
7
(declare-var sum_collapse_int_test.In12_1_1 Int)
8
(declare-var sum_collapse_int_test.In12_1_2 Int)
9
(declare-var sum_collapse_int_test.In12_1_3 Int)
10
(declare-var sum_collapse_int_test.In13_1_1 Int)
11
(declare-var sum_collapse_int_test.In13_1_2 Int)
12
(declare-var sum_collapse_int_test.In13_1_3 Int)
13
(declare-var sum_collapse_int_test.In13_1_4 Int)
14
(declare-var sum_collapse_int_test.In13_1_5 Int)
15
(declare-var sum_collapse_int_test.In13_1_6 Int)
16
(declare-var sum_collapse_int_test.In14_1_1 Int)
17
(declare-var sum_collapse_int_test.In14_1_2 Int)
18
(declare-var sum_collapse_int_test.In14_1_3 Int)
19
(declare-var sum_collapse_int_test.In14_1_4 Int)
20
(declare-var sum_collapse_int_test.In14_1_5 Int)
21
(declare-var sum_collapse_int_test.In14_1_6 Int)
22
(declare-var sum_collapse_int_test.In15_1_1 Int)
23
(declare-var sum_collapse_int_test.In15_1_2 Int)
24
(declare-var sum_collapse_int_test.In15_1_3 Int)
25
(declare-var sum_collapse_int_test.In15_1_4 Int)
26
(declare-var sum_collapse_int_test.In15_1_5 Int)
27
(declare-var sum_collapse_int_test.In15_1_6 Int)
28
(declare-var sum_collapse_int_test.In16_1_1 Int)
29
(declare-var sum_collapse_int_test.In16_1_2 Int)
30
(declare-var sum_collapse_int_test.In16_1_3 Int)
31
(declare-var sum_collapse_int_test.In16_1_4 Int)
32
(declare-var sum_collapse_int_test.In16_1_5 Int)
33
(declare-var sum_collapse_int_test.In16_1_6 Int)
34
(declare-var sum_collapse_int_test.Out9_1_1 Int)
35
(declare-var sum_collapse_int_test.Out10_2_1 Int)
36
(declare-var sum_collapse_int_test.Out11_3_1 Int)
37
(declare-var sum_collapse_int_test.Out12_4_1 Int)
38
(declare-var sum_collapse_int_test.Out13_5_1 Int)
39
(declare-var sum_collapse_int_test.Out13_5_2 Int)
40
(declare-var sum_collapse_int_test.Out13_5_3 Int)
41
(declare-var sum_collapse_int_test.Out14_6_1 Int)
42
(declare-var sum_collapse_int_test.Out14_6_2 Int)
43
(declare-var sum_collapse_int_test.Out14_6_3 Int)
44
(declare-var sum_collapse_int_test.Out15_7_1 Int)
45
(declare-var sum_collapse_int_test.Out15_7_2 Int)
46
(declare-var sum_collapse_int_test.Out16_8_1 Int)
47
(declare-var sum_collapse_int_test.Out16_8_2 Int)
48
(declare-var sum_collapse_int_test.ni_0._arrow._first_c Bool)
49
(declare-var sum_collapse_int_test.ni_0._arrow._first_m Bool)
50
(declare-var sum_collapse_int_test.ni_0._arrow._first_x Bool)
51
(declare-var sum_collapse_int_test.Sum10_1_1 Int)
52
(declare-var sum_collapse_int_test.Sum10_1_2 Int)
53
(declare-var sum_collapse_int_test.Sum10_1_3 Int)
54
(declare-var sum_collapse_int_test.Sum11_1_1 Int)
55
(declare-var sum_collapse_int_test.Sum11_1_2 Int)
56
(declare-var sum_collapse_int_test.Sum11_1_3 Int)
57
(declare-var sum_collapse_int_test.Sum12_1_1 Int)
58
(declare-var sum_collapse_int_test.Sum12_1_2 Int)
59
(declare-var sum_collapse_int_test.Sum13_1_1 Int)
60
(declare-var sum_collapse_int_test.Sum13_1_2 Int)
61
(declare-var sum_collapse_int_test.Sum18_1_1 Int)
62
(declare-var sum_collapse_int_test.Sum19_1_1 Int)
63
(declare-var sum_collapse_int_test.Sum8_1_1 Int)
64
(declare-var sum_collapse_int_test.Sum9_1_1 Int)
65
(declare-var sum_collapse_int_test.__sum_collapse_int_test_1 Bool)
66
(declare-var sum_collapse_int_test.i_virtual_local Real)
67
(declare-rel sum_collapse_int_test_reset (Bool Bool))
68
(declare-rel sum_collapse_int_test_step (Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Bool Bool))
69

    
70
(rule (=> 
71
  (and 
72
       
73
       (= sum_collapse_int_test.ni_0._arrow._first_m true)
74
  )
75
  (sum_collapse_int_test_reset sum_collapse_int_test.ni_0._arrow._first_c
76
                               sum_collapse_int_test.ni_0._arrow._first_m)
77
))
78

    
79
(rule (=> 
80
  (and (= sum_collapse_int_test.ni_0._arrow._first_m sum_collapse_int_test.ni_0._arrow._first_c)
81
       (and (= sum_collapse_int_test.__sum_collapse_int_test_1 (ite sum_collapse_int_test.ni_0._arrow._first_m true false))
82
            (= sum_collapse_int_test.ni_0._arrow._first_x false))
83
       (and (or (not (= sum_collapse_int_test.__sum_collapse_int_test_1 true))
84
               (= sum_collapse_int_test.i_virtual_local 0.0))
85
            (or (not (= sum_collapse_int_test.__sum_collapse_int_test_1 false))
86
               (= sum_collapse_int_test.i_virtual_local 1.0))
87
       )
88
       (= sum_collapse_int_test.Sum9_1_1 (- sum_collapse_int_test.In10_1_1))
89
       (= sum_collapse_int_test.Sum8_1_1 sum_collapse_int_test.In9_1_1)
90
       (= sum_collapse_int_test.Sum19_1_1 (- (- (- sum_collapse_int_test.In12_1_1) sum_collapse_int_test.In12_1_2) sum_collapse_int_test.In12_1_3))
91
       (= sum_collapse_int_test.Sum18_1_1 (+ (+ sum_collapse_int_test.In11_1_1 sum_collapse_int_test.In11_1_2) sum_collapse_int_test.In11_1_3))
92
       (= sum_collapse_int_test.Sum13_1_2 (- (- (- sum_collapse_int_test.In16_1_4) sum_collapse_int_test.In16_1_5) sum_collapse_int_test.In16_1_6))
93
       (= sum_collapse_int_test.Sum13_1_1 (- (- (- sum_collapse_int_test.In16_1_1) sum_collapse_int_test.In16_1_2) sum_collapse_int_test.In16_1_3))
94
       (= sum_collapse_int_test.Sum12_1_2 (+ (+ sum_collapse_int_test.In15_1_4 sum_collapse_int_test.In15_1_5) sum_collapse_int_test.In15_1_6))
95
       (= sum_collapse_int_test.Sum12_1_1 (+ (+ sum_collapse_int_test.In15_1_1 sum_collapse_int_test.In15_1_2) sum_collapse_int_test.In15_1_3))
96
       (= sum_collapse_int_test.Sum11_1_3 (- (- sum_collapse_int_test.In14_1_3) sum_collapse_int_test.In14_1_6))
97
       (= sum_collapse_int_test.Sum11_1_2 (- (- sum_collapse_int_test.In14_1_2) sum_collapse_int_test.In14_1_5))
98
       (= sum_collapse_int_test.Sum11_1_1 (- (- sum_collapse_int_test.In14_1_1) sum_collapse_int_test.In14_1_4))
99
       (= sum_collapse_int_test.Sum10_1_3 (+ sum_collapse_int_test.In13_1_3 sum_collapse_int_test.In13_1_6))
100
       (= sum_collapse_int_test.Sum10_1_2 (+ sum_collapse_int_test.In13_1_2 sum_collapse_int_test.In13_1_5))
101
       (= sum_collapse_int_test.Sum10_1_1 (+ sum_collapse_int_test.In13_1_1 sum_collapse_int_test.In13_1_4))
102
       (= sum_collapse_int_test.Out9_1_1 sum_collapse_int_test.Sum8_1_1)
103
       (= sum_collapse_int_test.Out16_8_2 sum_collapse_int_test.Sum13_1_2)
104
       (= sum_collapse_int_test.Out16_8_1 sum_collapse_int_test.Sum13_1_1)
105
       (= sum_collapse_int_test.Out15_7_2 sum_collapse_int_test.Sum12_1_2)
106
       (= sum_collapse_int_test.Out15_7_1 sum_collapse_int_test.Sum12_1_1)
107
       (= sum_collapse_int_test.Out14_6_3 sum_collapse_int_test.Sum11_1_3)
108
       (= sum_collapse_int_test.Out14_6_2 sum_collapse_int_test.Sum11_1_2)
109
       (= sum_collapse_int_test.Out14_6_1 sum_collapse_int_test.Sum11_1_1)
110
       (= sum_collapse_int_test.Out13_5_3 sum_collapse_int_test.Sum10_1_3)
111
       (= sum_collapse_int_test.Out13_5_2 sum_collapse_int_test.Sum10_1_2)
112
       (= sum_collapse_int_test.Out13_5_1 sum_collapse_int_test.Sum10_1_1)
113
       (= sum_collapse_int_test.Out12_4_1 sum_collapse_int_test.Sum19_1_1)
114
       (= sum_collapse_int_test.Out11_3_1 sum_collapse_int_test.Sum18_1_1)
115
       (= sum_collapse_int_test.Out10_2_1 sum_collapse_int_test.Sum9_1_1)
116
       )
117
  (sum_collapse_int_test_step sum_collapse_int_test.In9_1_1
118
                              sum_collapse_int_test.In10_1_1
119
                              sum_collapse_int_test.In11_1_1
120
                              sum_collapse_int_test.In11_1_2
121
                              sum_collapse_int_test.In11_1_3
122
                              sum_collapse_int_test.In12_1_1
123
                              sum_collapse_int_test.In12_1_2
124
                              sum_collapse_int_test.In12_1_3
125
                              sum_collapse_int_test.In13_1_1
126
                              sum_collapse_int_test.In13_1_2
127
                              sum_collapse_int_test.In13_1_3
128
                              sum_collapse_int_test.In13_1_4
129
                              sum_collapse_int_test.In13_1_5
130
                              sum_collapse_int_test.In13_1_6
131
                              sum_collapse_int_test.In14_1_1
132
                              sum_collapse_int_test.In14_1_2
133
                              sum_collapse_int_test.In14_1_3
134
                              sum_collapse_int_test.In14_1_4
135
                              sum_collapse_int_test.In14_1_5
136
                              sum_collapse_int_test.In14_1_6
137
                              sum_collapse_int_test.In15_1_1
138
                              sum_collapse_int_test.In15_1_2
139
                              sum_collapse_int_test.In15_1_3
140
                              sum_collapse_int_test.In15_1_4
141
                              sum_collapse_int_test.In15_1_5
142
                              sum_collapse_int_test.In15_1_6
143
                              sum_collapse_int_test.In16_1_1
144
                              sum_collapse_int_test.In16_1_2
145
                              sum_collapse_int_test.In16_1_3
146
                              sum_collapse_int_test.In16_1_4
147
                              sum_collapse_int_test.In16_1_5
148
                              sum_collapse_int_test.In16_1_6
149
                              sum_collapse_int_test.Out9_1_1
150
                              sum_collapse_int_test.Out10_2_1
151
                              sum_collapse_int_test.Out11_3_1
152
                              sum_collapse_int_test.Out12_4_1
153
                              sum_collapse_int_test.Out13_5_1
154
                              sum_collapse_int_test.Out13_5_2
155
                              sum_collapse_int_test.Out13_5_3
156
                              sum_collapse_int_test.Out14_6_1
157
                              sum_collapse_int_test.Out14_6_2
158
                              sum_collapse_int_test.Out14_6_3
159
                              sum_collapse_int_test.Out15_7_1
160
                              sum_collapse_int_test.Out15_7_2
161
                              sum_collapse_int_test.Out16_8_1
162
                              sum_collapse_int_test.Out16_8_2
163
                              sum_collapse_int_test.ni_0._arrow._first_c
164
                              sum_collapse_int_test.ni_0._arrow._first_x)
165
))
166