Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_sum_collapse_bool_test / sum_collapse_bool_test.smt2 @ 6c3ea955

History | View | Annotate | Download (10.2 KB)

1
; sum_collapse_bool_test
2
(declare-var sum_collapse_bool_test.In17_1_1 Int)
3
(declare-var sum_collapse_bool_test.In18_1_1 Int)
4
(declare-var sum_collapse_bool_test.In19_1_1 Int)
5
(declare-var sum_collapse_bool_test.In19_1_2 Int)
6
(declare-var sum_collapse_bool_test.In19_1_3 Int)
7
(declare-var sum_collapse_bool_test.In20_1_1 Int)
8
(declare-var sum_collapse_bool_test.In20_1_2 Int)
9
(declare-var sum_collapse_bool_test.In20_1_3 Int)
10
(declare-var sum_collapse_bool_test.In21_1_1 Int)
11
(declare-var sum_collapse_bool_test.In21_1_2 Int)
12
(declare-var sum_collapse_bool_test.In21_1_3 Int)
13
(declare-var sum_collapse_bool_test.In21_1_4 Int)
14
(declare-var sum_collapse_bool_test.In21_1_5 Int)
15
(declare-var sum_collapse_bool_test.In21_1_6 Int)
16
(declare-var sum_collapse_bool_test.In22_1_1 Int)
17
(declare-var sum_collapse_bool_test.In22_1_2 Int)
18
(declare-var sum_collapse_bool_test.In22_1_3 Int)
19
(declare-var sum_collapse_bool_test.In22_1_4 Int)
20
(declare-var sum_collapse_bool_test.In22_1_5 Int)
21
(declare-var sum_collapse_bool_test.In22_1_6 Int)
22
(declare-var sum_collapse_bool_test.In23_1_1 Int)
23
(declare-var sum_collapse_bool_test.In23_1_2 Int)
24
(declare-var sum_collapse_bool_test.In23_1_3 Int)
25
(declare-var sum_collapse_bool_test.In23_1_4 Int)
26
(declare-var sum_collapse_bool_test.In23_1_5 Int)
27
(declare-var sum_collapse_bool_test.In23_1_6 Int)
28
(declare-var sum_collapse_bool_test.In24_1_1 Int)
29
(declare-var sum_collapse_bool_test.In24_1_2 Int)
30
(declare-var sum_collapse_bool_test.In24_1_3 Int)
31
(declare-var sum_collapse_bool_test.In24_1_4 Int)
32
(declare-var sum_collapse_bool_test.In24_1_5 Int)
33
(declare-var sum_collapse_bool_test.In24_1_6 Int)
34
(declare-var sum_collapse_bool_test.Out17_1_1 Int)
35
(declare-var sum_collapse_bool_test.Out18_2_1 Int)
36
(declare-var sum_collapse_bool_test.Out19_3_1 Int)
37
(declare-var sum_collapse_bool_test.Out20_4_1 Int)
38
(declare-var sum_collapse_bool_test.Out21_5_1 Int)
39
(declare-var sum_collapse_bool_test.Out21_5_2 Int)
40
(declare-var sum_collapse_bool_test.Out21_5_3 Int)
41
(declare-var sum_collapse_bool_test.Out22_6_1 Int)
42
(declare-var sum_collapse_bool_test.Out22_6_2 Int)
43
(declare-var sum_collapse_bool_test.Out22_6_3 Int)
44
(declare-var sum_collapse_bool_test.Out23_7_1 Int)
45
(declare-var sum_collapse_bool_test.Out23_7_2 Int)
46
(declare-var sum_collapse_bool_test.Out24_8_1 Int)
47
(declare-var sum_collapse_bool_test.Out24_8_2 Int)
48
(declare-var sum_collapse_bool_test.ni_0._arrow._first_c Bool)
49
(declare-var sum_collapse_bool_test.ni_0._arrow._first_m Bool)
50
(declare-var sum_collapse_bool_test.ni_0._arrow._first_x Bool)
51
(declare-var sum_collapse_bool_test.Sum14_1_1 Int)
52
(declare-var sum_collapse_bool_test.Sum14_1_2 Int)
53
(declare-var sum_collapse_bool_test.Sum14_1_3 Int)
54
(declare-var sum_collapse_bool_test.Sum15_1_1 Int)
55
(declare-var sum_collapse_bool_test.Sum15_1_2 Int)
56
(declare-var sum_collapse_bool_test.Sum15_1_3 Int)
57
(declare-var sum_collapse_bool_test.Sum16_1_1 Int)
58
(declare-var sum_collapse_bool_test.Sum17_1_1 Int)
59
(declare-var sum_collapse_bool_test.Sum20_1_1 Int)
60
(declare-var sum_collapse_bool_test.Sum21_1_1 Int)
61
(declare-var sum_collapse_bool_test.Sum22_1_1 Int)
62
(declare-var sum_collapse_bool_test.Sum22_1_2 Int)
63
(declare-var sum_collapse_bool_test.Sum23_1_1 Int)
64
(declare-var sum_collapse_bool_test.Sum23_1_2 Int)
65
(declare-var sum_collapse_bool_test.__sum_collapse_bool_test_1 Bool)
66
(declare-var sum_collapse_bool_test.i_virtual_local Real)
67
(declare-rel sum_collapse_bool_test_reset (Bool Bool))
68
(declare-rel sum_collapse_bool_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_bool_test.ni_0._arrow._first_m true)
74
  )
75
  (sum_collapse_bool_test_reset sum_collapse_bool_test.ni_0._arrow._first_c
76
                                sum_collapse_bool_test.ni_0._arrow._first_m)
77
))
78

    
79
(rule (=> 
80
  (and (= sum_collapse_bool_test.ni_0._arrow._first_m sum_collapse_bool_test.ni_0._arrow._first_c)
81
       (and (= sum_collapse_bool_test.__sum_collapse_bool_test_1 (ite sum_collapse_bool_test.ni_0._arrow._first_m true false))
82
            (= sum_collapse_bool_test.ni_0._arrow._first_x false))
83
       (and (or (not (= sum_collapse_bool_test.__sum_collapse_bool_test_1 true))
84
               (= sum_collapse_bool_test.i_virtual_local 0.0))
85
            (or (not (= sum_collapse_bool_test.__sum_collapse_bool_test_1 false))
86
               (= sum_collapse_bool_test.i_virtual_local 1.0))
87
       )
88
       (= sum_collapse_bool_test.Sum23_1_2 (- (- (- sum_collapse_bool_test.In24_1_4) sum_collapse_bool_test.In24_1_5) sum_collapse_bool_test.In24_1_6))
89
       (= sum_collapse_bool_test.Sum23_1_1 (- (- (- sum_collapse_bool_test.In24_1_1) sum_collapse_bool_test.In24_1_2) sum_collapse_bool_test.In24_1_3))
90
       (= sum_collapse_bool_test.Sum22_1_2 (+ (+ sum_collapse_bool_test.In23_1_4 sum_collapse_bool_test.In23_1_5) sum_collapse_bool_test.In23_1_6))
91
       (= sum_collapse_bool_test.Sum22_1_1 (+ (+ sum_collapse_bool_test.In23_1_1 sum_collapse_bool_test.In23_1_2) sum_collapse_bool_test.In23_1_3))
92
       (= sum_collapse_bool_test.Sum21_1_1 (- (- (- sum_collapse_bool_test.In20_1_1) sum_collapse_bool_test.In20_1_2) sum_collapse_bool_test.In20_1_3))
93
       (= sum_collapse_bool_test.Sum20_1_1 (+ (+ sum_collapse_bool_test.In19_1_1 sum_collapse_bool_test.In19_1_2) sum_collapse_bool_test.In19_1_3))
94
       (= sum_collapse_bool_test.Sum17_1_1 (- sum_collapse_bool_test.In18_1_1))
95
       (= sum_collapse_bool_test.Sum16_1_1 sum_collapse_bool_test.In17_1_1)
96
       (= sum_collapse_bool_test.Sum15_1_3 (- (- sum_collapse_bool_test.In22_1_3) sum_collapse_bool_test.In22_1_6))
97
       (= sum_collapse_bool_test.Sum15_1_2 (- (- sum_collapse_bool_test.In22_1_2) sum_collapse_bool_test.In22_1_5))
98
       (= sum_collapse_bool_test.Sum15_1_1 (- (- sum_collapse_bool_test.In22_1_1) sum_collapse_bool_test.In22_1_4))
99
       (= sum_collapse_bool_test.Sum14_1_3 (+ sum_collapse_bool_test.In21_1_3 sum_collapse_bool_test.In21_1_6))
100
       (= sum_collapse_bool_test.Sum14_1_2 (+ sum_collapse_bool_test.In21_1_2 sum_collapse_bool_test.In21_1_5))
101
       (= sum_collapse_bool_test.Sum14_1_1 (+ sum_collapse_bool_test.In21_1_1 sum_collapse_bool_test.In21_1_4))
102
       (= sum_collapse_bool_test.Out24_8_2 sum_collapse_bool_test.Sum23_1_2)
103
       (= sum_collapse_bool_test.Out24_8_1 sum_collapse_bool_test.Sum23_1_1)
104
       (= sum_collapse_bool_test.Out23_7_2 sum_collapse_bool_test.Sum22_1_2)
105
       (= sum_collapse_bool_test.Out23_7_1 sum_collapse_bool_test.Sum22_1_1)
106
       (= sum_collapse_bool_test.Out22_6_3 sum_collapse_bool_test.Sum15_1_3)
107
       (= sum_collapse_bool_test.Out22_6_2 sum_collapse_bool_test.Sum15_1_2)
108
       (= sum_collapse_bool_test.Out22_6_1 sum_collapse_bool_test.Sum15_1_1)
109
       (= sum_collapse_bool_test.Out21_5_3 sum_collapse_bool_test.Sum14_1_3)
110
       (= sum_collapse_bool_test.Out21_5_2 sum_collapse_bool_test.Sum14_1_2)
111
       (= sum_collapse_bool_test.Out21_5_1 sum_collapse_bool_test.Sum14_1_1)
112
       (= sum_collapse_bool_test.Out20_4_1 sum_collapse_bool_test.Sum21_1_1)
113
       (= sum_collapse_bool_test.Out19_3_1 sum_collapse_bool_test.Sum20_1_1)
114
       (= sum_collapse_bool_test.Out18_2_1 sum_collapse_bool_test.Sum17_1_1)
115
       (= sum_collapse_bool_test.Out17_1_1 sum_collapse_bool_test.Sum16_1_1)
116
       )
117
  (sum_collapse_bool_test_step sum_collapse_bool_test.In17_1_1
118
                               sum_collapse_bool_test.In18_1_1
119
                               sum_collapse_bool_test.In19_1_1
120
                               sum_collapse_bool_test.In19_1_2
121
                               sum_collapse_bool_test.In19_1_3
122
                               sum_collapse_bool_test.In20_1_1
123
                               sum_collapse_bool_test.In20_1_2
124
                               sum_collapse_bool_test.In20_1_3
125
                               sum_collapse_bool_test.In21_1_1
126
                               sum_collapse_bool_test.In21_1_2
127
                               sum_collapse_bool_test.In21_1_3
128
                               sum_collapse_bool_test.In21_1_4
129
                               sum_collapse_bool_test.In21_1_5
130
                               sum_collapse_bool_test.In21_1_6
131
                               sum_collapse_bool_test.In22_1_1
132
                               sum_collapse_bool_test.In22_1_2
133
                               sum_collapse_bool_test.In22_1_3
134
                               sum_collapse_bool_test.In22_1_4
135
                               sum_collapse_bool_test.In22_1_5
136
                               sum_collapse_bool_test.In22_1_6
137
                               sum_collapse_bool_test.In23_1_1
138
                               sum_collapse_bool_test.In23_1_2
139
                               sum_collapse_bool_test.In23_1_3
140
                               sum_collapse_bool_test.In23_1_4
141
                               sum_collapse_bool_test.In23_1_5
142
                               sum_collapse_bool_test.In23_1_6
143
                               sum_collapse_bool_test.In24_1_1
144
                               sum_collapse_bool_test.In24_1_2
145
                               sum_collapse_bool_test.In24_1_3
146
                               sum_collapse_bool_test.In24_1_4
147
                               sum_collapse_bool_test.In24_1_5
148
                               sum_collapse_bool_test.In24_1_6
149
                               sum_collapse_bool_test.Out17_1_1
150
                               sum_collapse_bool_test.Out18_2_1
151
                               sum_collapse_bool_test.Out19_3_1
152
                               sum_collapse_bool_test.Out20_4_1
153
                               sum_collapse_bool_test.Out21_5_1
154
                               sum_collapse_bool_test.Out21_5_2
155
                               sum_collapse_bool_test.Out21_5_3
156
                               sum_collapse_bool_test.Out22_6_1
157
                               sum_collapse_bool_test.Out22_6_2
158
                               sum_collapse_bool_test.Out22_6_3
159
                               sum_collapse_bool_test.Out23_7_1
160
                               sum_collapse_bool_test.Out23_7_2
161
                               sum_collapse_bool_test.Out24_8_1
162
                               sum_collapse_bool_test.Out24_8_2
163
                               sum_collapse_bool_test.ni_0._arrow._first_c
164
                               sum_collapse_bool_test.ni_0._arrow._first_x)
165
))
166