|
1 | 1 | ; solver scope 0 |
2 | | -(declare-const tmp (_ BitVec 2)) |
3 | | -(declare-const tmp_0 (_ BitVec 2)) |
4 | | -(declare-const tmp_1 (_ BitVec 2)) |
5 | | -(assert (let ((tmp_2 ((_ extract 0 0) tmp))) |
6 | | - (let ((tmp_3 ((_ extract 0 0) tmp_0))) |
7 | | - (let ((tmp_4 ((_ extract 0 0) tmp_1))) |
| 2 | +(declare-const a (_ BitVec 2)) |
| 3 | +(declare-const b (_ BitVec 2)) |
| 4 | +(declare-const c (_ BitVec 2)) |
| 5 | +(assert (let ((tmp_2 ((_ extract 0 0) a))) |
| 6 | + (let ((tmp_3 ((_ extract 0 0) b))) |
| 7 | + (let ((tmp_4 ((_ extract 0 0) c))) |
8 | 8 | (let ((tmp_5 (bvand tmp_4 tmp_3))) |
9 | 9 | (let ((tmp_6 (bvxor tmp_5 #b1))) |
10 | 10 | (let ((tmp_7 (bvxor tmp_3 #b1))) |
|
19 | 19 | (let ((tmp_16 (bvand tmp_15 tmp_14))) |
20 | 20 | (let ((tmp_17 (bvxor tmp_16 #b1))) |
21 | 21 | (let ((tmp_18 (bvand tmp_17 tmp_13))) |
22 | | - (let ((tmp_19 ((_ extract 1 1) tmp))) |
23 | | - (let ((tmp_20 ((_ extract 1 1) tmp_0))) |
24 | | - (let ((tmp_21 ((_ extract 1 1) tmp_1))) |
| 22 | + (let ((tmp_19 ((_ extract 1 1) a))) |
| 23 | + (let ((tmp_20 ((_ extract 1 1) b))) |
| 24 | + (let ((tmp_21 ((_ extract 1 1) c))) |
25 | 25 | (let ((tmp_22 (bvand tmp_21 tmp_20))) |
26 | 26 | (let ((tmp_23 (bvxor tmp_22 #b1))) |
27 | 27 | (let ((tmp_24 (bvxor tmp_20 #b1))) |
|
53 | 53 | (let ((tmp_50 (bvand tmp_49 tmp_47))) |
54 | 54 | (let ((tmp_51 (concat tmp_50 tmp_43))) |
55 | 55 | (let ((tmp_52 (concat tmp_51 tmp_18))) |
56 | | - (let ((tmp_53 (concat #b0 tmp_1))) |
57 | | - (let ((tmp_54 (concat #b0 tmp_0))) |
58 | | - (let ((tmp_55 (concat #b0 tmp))) |
| 56 | + (let ((tmp_53 (concat #b0 c))) |
| 57 | + (let ((tmp_54 (concat #b0 b))) |
| 58 | + (let ((tmp_55 (concat #b0 a))) |
59 | 59 | (let ((tmp_56 (bvadd tmp_55 tmp_54))) |
60 | 60 | (let ((tmp_57 (bvadd tmp_56 tmp_53))) |
61 | 61 | (let ((tmp_58 (distinct tmp_57 tmp_52))) |
|
0 commit comments