SBVTestSuite/GoldFiles/barrelRotate_Left_Int64_Word64.gold

2 [GOOD] ; Automatically generated by SBV. Do not edit.
3 [GOOD] (set-option :print-success true)
4 [GOOD] (set-option :global-declarations true)
5 [GOOD] (set-option :diagnostic-output-channel "stdout")
6 [GOOD] (set-option :produce-models true)
7 [GOOD] (set-logic QF_UFBV)
8 [GOOD] ; --- uninterpreted sorts ---
9 [GOOD] ; --- tuples ---
10 [GOOD] ; --- sums ---
11 [GOOD] ; --- literal constants ---
12 [GOOD] (define-fun s2 () (_ BitVec 64) #x0000000000000040)
13 [GOOD] (define-fun s5 () (_ BitVec 1) #b0)
14 [GOOD] (define-fun s91 () (_ BitVec 64) #x0000000000000000)
15 [GOOD] ; --- skolem constants ---
16 [GOOD] (declare-fun s0 () (_ BitVec 64))
17 [GOOD] (declare-fun s1 () (_ BitVec 64))
18 [GOOD] ; --- constant tables ---
19 [GOOD] ; --- skolemized tables ---
20 [GOOD] (declare-fun table0 ((_ BitVec 64)) (_ BitVec 64))
21 [GOOD] ; --- arrays ---
22 [GOOD] ; --- uninterpreted constants ---
23 [GOOD] ; --- user given axioms ---
24 [GOOD] ; --- formula ---
25 [GOOD] (define-fun s3 () (_ BitVec 64) (bvurem s1 s2))
26 [GOOD] (define-fun s4 () (_ BitVec 1) ((_ extract 5 5) s3))
27 [GOOD] (define-fun s6 () Bool (distinct s4 s5))
28 [GOOD] (define-fun s7 () (_ BitVec 1) ((_ extract 4 4) s3))
29 [GOOD] (define-fun s8 () Bool (distinct s5 s7))
30 [GOOD] (define-fun s9 () (_ BitVec 1) ((_ extract 3 3) s3))
31 [GOOD] (define-fun s10 () Bool (distinct s5 s9))
32 [GOOD] (define-fun s11 () (_ BitVec 1) ((_ extract 2 2) s3))
33 [GOOD] (define-fun s12 () Bool (distinct s5 s11))
34 [GOOD] (define-fun s13 () (_ BitVec 1) ((_ extract 1 1) s3))
35 [GOOD] (define-fun s14 () Bool (distinct s5 s13))
36 [GOOD] (define-fun s15 () (_ BitVec 1) ((_ extract 0 0) s3))
37 [GOOD] (define-fun s16 () Bool (distinct s5 s15))
38 [GOOD] (define-fun s17 () (_ BitVec 64) ((_ rotate_left 1) s0))
39 [GOOD] (define-fun s18 () (_ BitVec 64) (ite s16 s17 s0))
40 [GOOD] (define-fun s19 () (_ BitVec 64) ((_ rotate_left 2) s18))
41 [GOOD] (define-fun s20 () (_ BitVec 64) (ite s14 s19 s18))
42 [GOOD] (define-fun s21 () (_ BitVec 64) ((_ rotate_left 4) s20))
43 [GOOD] (define-fun s22 () (_ BitVec 64) (ite s12 s21 s20))
44 [GOOD] (define-fun s23 () (_ BitVec 64) ((_ rotate_left 8) s22))
45 [GOOD] (define-fun s24 () (_ BitVec 64) (ite s10 s23 s22))
46 [GOOD] (define-fun s25 () (_ BitVec 64) ((_ rotate_left 16) s24))
47 [GOOD] (define-fun s26 () (_ BitVec 64) (ite s8 s25 s24))
48 [GOOD] (define-fun s27 () (_ BitVec 64) ((_ rotate_left 32) s26))
49 [GOOD] (define-fun s28 () (_ BitVec 64) (ite s6 s27 s26))
50 [GOOD] (define-fun s29 () (_ BitVec 64) ((_ rotate_left 2) s0))
51 [GOOD] (define-fun s30 () (_ BitVec 64) ((_ rotate_left 3) s0))
52 [GOOD] (define-fun s31 () (_ BitVec 64) ((_ rotate_left 4) s0))
53 [GOOD] (define-fun s32 () (_ BitVec 64) ((_ rotate_left 5) s0))
54 [GOOD] (define-fun s33 () (_ BitVec 64) ((_ rotate_left 6) s0))
55 [GOOD] (define-fun s34 () (_ BitVec 64) ((_ rotate_left 7) s0))
56 [GOOD] (define-fun s35 () (_ BitVec 64) ((_ rotate_left 8) s0))
57 [GOOD] (define-fun s36 () (_ BitVec 64) ((_ rotate_left 9) s0))
58 [GOOD] (define-fun s37 () (_ BitVec 64) ((_ rotate_left 10) s0))
59 [GOOD] (define-fun s38 () (_ BitVec 64) ((_ rotate_left 11) s0))
60 [GOOD] (define-fun s39 () (_ BitVec 64) ((_ rotate_left 12) s0))
61 [GOOD] (define-fun s40 () (_ BitVec 64) ((_ rotate_left 13) s0))
62 [GOOD] (define-fun s41 () (_ BitVec 64) ((_ rotate_left 14) s0))
63 [GOOD] (define-fun s42 () (_ BitVec 64) ((_ rotate_left 15) s0))
64 [GOOD] (define-fun s43 () (_ BitVec 64) ((_ rotate_left 16) s0))
65 [GOOD] (define-fun s44 () (_ BitVec 64) ((_ rotate_left 17) s0))
66 [GOOD] (define-fun s45 () (_ BitVec 64) ((_ rotate_left 18) s0))
67 [GOOD] (define-fun s46 () (_ BitVec 64) ((_ rotate_left 19) s0))
68 [GOOD] (define-fun s47 () (_ BitVec 64) ((_ rotate_left 20) s0))
69 [GOOD] (define-fun s48 () (_ BitVec 64) ((_ rotate_left 21) s0))
70 [GOOD] (define-fun s49 () (_ BitVec 64) ((_ rotate_left 22) s0))
71 [GOOD] (define-fun s50 () (_ BitVec 64) ((_ rotate_left 23) s0))
72 [GOOD] (define-fun s51 () (_ BitVec 64) ((_ rotate_left 24) s0))
73 [GOOD] (define-fun s52 () (_ BitVec 64) ((_ rotate_left 25) s0))
74 [GOOD] (define-fun s53 () (_ BitVec 64) ((_ rotate_left 26) s0))
75 [GOOD] (define-fun s54 () (_ BitVec 64) ((_ rotate_left 27) s0))
76 [GOOD] (define-fun s55 () (_ BitVec 64) ((_ rotate_left 28) s0))
77 [GOOD] (define-fun s56 () (_ BitVec 64) ((_ rotate_left 29) s0))
78 [GOOD] (define-fun s57 () (_ BitVec 64) ((_ rotate_left 30) s0))
79 [GOOD] (define-fun s58 () (_ BitVec 64) ((_ rotate_left 31) s0))
80 [GOOD] (define-fun s59 () (_ BitVec 64) ((_ rotate_left 32) s0))
81 [GOOD] (define-fun s60 () (_ BitVec 64) ((_ rotate_left 33) s0))
82 [GOOD] (define-fun s61 () (_ BitVec 64) ((_ rotate_left 34) s0))
83 [GOOD] (define-fun s62 () (_ BitVec 64) ((_ rotate_left 35) s0))
84 [GOOD] (define-fun s63 () (_ BitVec 64) ((_ rotate_left 36) s0))
85 [GOOD] (define-fun s64 () (_ BitVec 64) ((_ rotate_left 37) s0))
86 [GOOD] (define-fun s65 () (_ BitVec 64) ((_ rotate_left 38) s0))
87 [GOOD] (define-fun s66 () (_ BitVec 64) ((_ rotate_left 39) s0))
88 [GOOD] (define-fun s67 () (_ BitVec 64) ((_ rotate_left 40) s0))
89 [GOOD] (define-fun s68 () (_ BitVec 64) ((_ rotate_left 41) s0))
90 [GOOD] (define-fun s69 () (_ BitVec 64) ((_ rotate_left 42) s0))
91 [GOOD] (define-fun s70 () (_ BitVec 64) ((_ rotate_left 43) s0))
92 [GOOD] (define-fun s71 () (_ BitVec 64) ((_ rotate_left 44) s0))
93 [GOOD] (define-fun s72 () (_ BitVec 64) ((_ rotate_left 45) s0))
94 [GOOD] (define-fun s73 () (_ BitVec 64) ((_ rotate_left 46) s0))
95 [GOOD] (define-fun s74 () (_ BitVec 64) ((_ rotate_left 47) s0))
96 [GOOD] (define-fun s75 () (_ BitVec 64) ((_ rotate_left 48) s0))
97 [GOOD] (define-fun s76 () (_ BitVec 64) ((_ rotate_left 49) s0))
98 [GOOD] (define-fun s77 () (_ BitVec 64) ((_ rotate_left 50) s0))
99 [GOOD] (define-fun s78 () (_ BitVec 64) ((_ rotate_left 51) s0))
100 [GOOD] (define-fun s79 () (_ BitVec 64) ((_ rotate_left 52) s0))
101 [GOOD] (define-fun s80 () (_ BitVec 64) ((_ rotate_left 53) s0))
102 [GOOD] (define-fun s81 () (_ BitVec 64) ((_ rotate_left 54) s0))
103 [GOOD] (define-fun s82 () (_ BitVec 64) ((_ rotate_left 55) s0))
104 [GOOD] (define-fun s83 () (_ BitVec 64) ((_ rotate_left 56) s0))
105 [GOOD] (define-fun s84 () (_ BitVec 64) ((_ rotate_left 57) s0))
106 [GOOD] (define-fun s85 () (_ BitVec 64) ((_ rotate_left 58) s0))
107 [GOOD] (define-fun s86 () (_ BitVec 64) ((_ rotate_left 59) s0))
108 [GOOD] (define-fun s87 () (_ BitVec 64) ((_ rotate_left 60) s0))
109 [GOOD] (define-fun s88 () (_ BitVec 64) ((_ rotate_left 61) s0))
110 [GOOD] (define-fun s89 () (_ BitVec 64) ((_ rotate_left 62) s0))
111 [GOOD] (define-fun s90 () (_ BitVec 64) ((_ rotate_left 63) s0))
112 [GOOD] (define-fun s92 () (_ BitVec 64) (ite (bvule #x0000000000000040 s3) s91 (table0 s3)))
113 [GOOD] (define-fun s93 () Bool (= s28 s92))
114 [GOOD] (assert (= (table0 #x0000000000000000) s0))
115 [GOOD] (assert (= (table0 #x0000000000000001) s17))
116 [GOOD] (assert (= (table0 #x0000000000000002) s29))
117 [GOOD] (assert (= (table0 #x0000000000000003) s30))
118 [GOOD] (assert (= (table0 #x0000000000000004) s31))
119 [GOOD] (assert (= (table0 #x0000000000000005) s32))
120 [GOOD] (assert (= (table0 #x0000000000000006) s33))
121 [GOOD] (assert (= (table0 #x0000000000000007) s34))
122 [GOOD] (assert (= (table0 #x0000000000000008) s35))
123 [GOOD] (assert (= (table0 #x0000000000000009) s36))
124 [GOOD] (assert (= (table0 #x000000000000000a) s37))
125 [GOOD] (assert (= (table0 #x000000000000000b) s38))
126 [GOOD] (assert (= (table0 #x000000000000000c) s39))
127 [GOOD] (assert (= (table0 #x000000000000000d) s40))
128 [GOOD] (assert (= (table0 #x000000000000000e) s41))
129 [GOOD] (assert (= (table0 #x000000000000000f) s42))
130 [GOOD] (assert (= (table0 #x0000000000000010) s43))
131 [GOOD] (assert (= (table0 #x0000000000000011) s44))
132 [GOOD] (assert (= (table0 #x0000000000000012) s45))
133 [GOOD] (assert (= (table0 #x0000000000000013) s46))
134 [GOOD] (assert (= (table0 #x0000000000000014) s47))
135 [GOOD] (assert (= (table0 #x0000000000000015) s48))
136 [GOOD] (assert (= (table0 #x0000000000000016) s49))
137 [GOOD] (assert (= (table0 #x0000000000000017) s50))
138 [GOOD] (assert (= (table0 #x0000000000000018) s51))
139 [GOOD] (assert (= (table0 #x0000000000000019) s52))
140 [GOOD] (assert (= (table0 #x000000000000001a) s53))
141 [GOOD] (assert (= (table0 #x000000000000001b) s54))
142 [GOOD] (assert (= (table0 #x000000000000001c) s55))
143 [GOOD] (assert (= (table0 #x000000000000001d) s56))
144 [GOOD] (assert (= (table0 #x000000000000001e) s57))
145 [GOOD] (assert (= (table0 #x000000000000001f) s58))
146 [GOOD] (assert (= (table0 #x0000000000000020) s59))
147 [GOOD] (assert (= (table0 #x0000000000000021) s60))
148 [GOOD] (assert (= (table0 #x0000000000000022) s61))
149 [GOOD] (assert (= (table0 #x0000000000000023) s62))
150 [GOOD] (assert (= (table0 #x0000000000000024) s63))
151 [GOOD] (assert (= (table0 #x0000000000000025) s64))
152 [GOOD] (assert (= (table0 #x0000000000000026) s65))
153 [GOOD] (assert (= (table0 #x0000000000000027) s66))
154 [GOOD] (assert (= (table0 #x0000000000000028) s67))
155 [GOOD] (assert (= (table0 #x0000000000000029) s68))
156 [GOOD] (assert (= (table0 #x000000000000002a) s69))
157 [GOOD] (assert (= (table0 #x000000000000002b) s70))
158 [GOOD] (assert (= (table0 #x000000000000002c) s71))
159 [GOOD] (assert (= (table0 #x000000000000002d) s72))
160 [GOOD] (assert (= (table0 #x000000000000002e) s73))
161 [GOOD] (assert (= (table0 #x000000000000002f) s74))
162 [GOOD] (assert (= (table0 #x0000000000000030) s75))
163 [GOOD] (assert (= (table0 #x0000000000000031) s76))
164 [GOOD] (assert (= (table0 #x0000000000000032) s77))
165 [GOOD] (assert (= (table0 #x0000000000000033) s78))
166 [GOOD] (assert (= (table0 #x0000000000000034) s79))
167 [GOOD] (assert (= (table0 #x0000000000000035) s80))
168 [GOOD] (assert (= (table0 #x0000000000000036) s81))
169 [GOOD] (assert (= (table0 #x0000000000000037) s82))
170 [GOOD] (assert (= (table0 #x0000000000000038) s83))
171 [GOOD] (assert (= (table0 #x0000000000000039) s84))
172 [GOOD] (assert (= (table0 #x000000000000003a) s85))
173 [GOOD] (assert (= (table0 #x000000000000003b) s86))
174 [GOOD] (assert (= (table0 #x000000000000003c) s87))
175 [GOOD] (assert (= (table0 #x000000000000003d) s88))
176 [GOOD] (assert (= (table0 #x000000000000003e) s89))
177 [GOOD] (assert (= (table0 #x000000000000003f) s90))
178 [GOOD] (assert (not s93))