regress/mantis/0034.a.ys

1 (define |state.cx!0!0| :: real)
2 (define |state.cx!0!1| :: real)
3 (define |state.cx!0!2| :: real)
4 (define |state.cx!0!3| :: real)
5 (define |state.cx!1!0| :: real)
6 (define |state.cx!1!1| :: real)
7 (define |state.cx!1!2| :: real)
8 (define |state.cx!1!3| :: real)
9 (define |state.cx!2!0| :: real)
10 (define |state.cx!2!1| :: real)
11 (define |state.cx!2!2| :: real)
12 (define |state.cx!2!3| :: real)
13 (define |state.cx!3!0| :: real)
14 (define |state.cx!3!1| :: real)
15 (define |state.cx!3!2| :: real)
16 (define |state.cx!3!3| :: real)
17 (define |state.cy!0!0| :: real)
18 (define |state.cy!0!1| :: real)
19 (define |state.cy!0!2| :: real)
20 (define |state.cy!0!3| :: real)
21 (define |state.cy!1!0| :: real)
22 (define |state.cy!1!1| :: real)
23 (define |state.cy!1!2| :: real)
24 (define |state.cy!1!3| :: real)
25 (define |state.cy!2!0| :: real)
26 (define |state.cy!2!1| :: real)
27 (define |state.cy!2!2| :: real)
28 (define |state.cy!2!3| :: real)
29 (define |state.cy!3!0| :: real)
30 (define |state.cy!3!1| :: real)
31 (define |state.cy!3!2| :: real)
32 (define |state.cy!3!3| :: real)
33 (define |state.good_p!0| :: bool)
34 (define |state.good_p!1| :: bool)
35 (define |state.good_p!2| :: bool)
36 (define |state.good_p!3| :: bool)
37 (define |state.good_r!0| :: bool)
38 (define |state.good_r!1| :: bool)
39 (define |state.good_r!2| :: bool)
40 (define |state.good_r!3| :: bool)
41 (define |state.v!0| :: real)
42 (define |state.v!1| :: real)
43 (define |state.v!2| :: real)
44 (define |state.v!3| :: real)
45 (define |state.round| :: real)
46 (define |state.source| :: real)
47 (define |state.val| :: real)
96 …state.source| |next.source|) (= |state.val| |next.val|) (or (and (= |state.round| 0) (or (not |sta…
98 …state.source| 4) |state.good_p!3| (ite (= |state.source| 3) |state.good_p!2| (ite (= |state.source…
105 (assert (not (and (not |state.good_p!2|) (not |state.good_p!3|))))
106 (assert (not (and (not |state.good_r!0|) (not |state.good_r!1|))))
107 (assert (not (and (not |state.good_r!0|) (not |state.good_r!2|))))
108 (assert (not (and (not |state.good_r!0|) (not |state.good_r!3|))))
110 (assert (not (= |state.round| 2)))
112 (assert (not (and (not |state.good_p!1|) (not |state.good_p!3|))))
114 …state.round| 2)) (not (and (not |state.good_p!1|) (not |state.good_p!3|))) |state.good_r!2| |state…
116 …state.round| 2)) (not (and (not |state.good_p!1|) (not |state.good_p!3|))) (not (and (not (= |stat…
123 …state.round| 2)) (not (and (not |state.good_p!1|) (not |state.good_p!3|))) (not (and (not (= |stat…
130 …state.round| 2)) (not (and (not |state.good_p!1|) (not |state.good_p!3|))) (not (and (not (= |stat…
137 …state.round| 2)) (not (and (not |state.good_p!1|) (not |state.good_p!3|))) (not (and (not (= |stat…