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