1(benchmark icbrtorinvalidvc.smt
2:source {
3Integer cube root algorithm icbrt(x), where x is an unsigned 32 bit integer.
4From the book "Hacker's delight" by Henry S. Warren, Jr., page 212
5We use "or" instead of "add" to increment values inside the loop.
6
7We try to show the invalid verification condition:
8y^3 == x or (y^3 < x and (y+1)^3 > x) holds, where y is the result.
9
10Contributed by Robert Brummayer (robert.brummayer@gmail.com)
11}
12:status sat
13:category { crafted }
14:logic QF_BV
15:extrafuns ((x BitVec[32]))
16:formula
17(let (?e2 bv30[5])
18(let (?e3 bv0[32])
19(let (?e4 bv1[32])
20(let (?e5 bv2[32])
21(let (?e6 bv3[32])
22(let (?e7 bv3[5])
23(let (?e8 (bvmul ?e3 ?e5))
24(let (?e9 (bvor ?e8 ?e4))
25(let (?e10 (bvmul ?e8 ?e6))
26(let (?e11 (bvmul ?e10 ?e9))
27(let (?e12 (bvor ?e11 ?e4))
28(let (?e13 (bvshl ?e12 (zero_extend[27] ?e2)))
29(let (?e14 (bvsub ?e2 ?e7))
30(let (?e15 (ite (bvuge x ?e13) bv1[1] bv0[1]))
31(let (?e16 (bvsub x ?e13))
32(let (?e17 (ite (= bv1[1] ?e15) ?e16 x))
33(let (?e18 (bvor ?e8 ?e4))
34(let (?e19 (ite (= bv1[1] ?e15) ?e18 ?e8))
35(let (?e20 (bvmul ?e19 ?e5))
36(let (?e21 (bvor ?e20 ?e4))
37(let (?e22 (bvmul ?e20 ?e6))
38(let (?e23 (bvmul ?e22 ?e21))
39(let (?e24 (bvor ?e23 ?e4))
40(let (?e25 (bvshl ?e24 (zero_extend[27] ?e14)))
41(let (?e26 (bvsub ?e14 ?e7))
42(let (?e27 (ite (bvuge ?e17 ?e25) bv1[1] bv0[1]))
43(let (?e28 (bvsub ?e17 ?e25))
44(let (?e29 (ite (= bv1[1] ?e27) ?e28 ?e17))
45(let (?e30 (bvor ?e20 ?e4))
46(let (?e31 (ite (= bv1[1] ?e27) ?e30 ?e20))
47(let (?e32 (bvmul ?e31 ?e5))
48(let (?e33 (bvor ?e32 ?e4))
49(let (?e34 (bvmul ?e32 ?e6))
50(let (?e35 (bvmul ?e34 ?e33))
51(let (?e36 (bvor ?e35 ?e4))
52(let (?e37 (bvshl ?e36 (zero_extend[27] ?e26)))
53(let (?e38 (bvsub ?e26 ?e7))
54(let (?e39 (ite (bvuge ?e29 ?e37) bv1[1] bv0[1]))
55(let (?e40 (bvsub ?e29 ?e37))
56(let (?e41 (ite (= bv1[1] ?e39) ?e40 ?e29))
57(let (?e42 (bvor ?e32 ?e4))
58(let (?e43 (ite (= bv1[1] ?e39) ?e42 ?e32))
59(let (?e44 (bvmul ?e43 ?e5))
60(let (?e45 (bvor ?e44 ?e4))
61(let (?e46 (bvmul ?e44 ?e6))
62(let (?e47 (bvmul ?e46 ?e45))
63(let (?e48 (bvor ?e47 ?e4))
64(let (?e49 (bvshl ?e48 (zero_extend[27] ?e38)))
65(let (?e50 (bvsub ?e38 ?e7))
66(let (?e51 (ite (bvuge ?e41 ?e49) bv1[1] bv0[1]))
67(let (?e52 (bvsub ?e41 ?e49))
68(let (?e53 (ite (= bv1[1] ?e51) ?e52 ?e41))
69(let (?e54 (bvor ?e44 ?e4))
70(let (?e55 (ite (= bv1[1] ?e51) ?e54 ?e44))
71(let (?e56 (bvmul ?e55 ?e5))
72(let (?e57 (bvor ?e56 ?e4))
73(let (?e58 (bvmul ?e56 ?e6))
74(let (?e59 (bvmul ?e58 ?e57))
75(let (?e60 (bvor ?e59 ?e4))
76(let (?e61 (bvshl ?e60 (zero_extend[27] ?e50)))
77(let (?e62 (bvsub ?e50 ?e7))
78(let (?e63 (ite (bvuge ?e53 ?e61) bv1[1] bv0[1]))
79(let (?e64 (bvsub ?e53 ?e61))
80(let (?e65 (ite (= bv1[1] ?e63) ?e64 ?e53))
81(let (?e66 (bvor ?e56 ?e4))
82(let (?e67 (ite (= bv1[1] ?e63) ?e66 ?e56))
83(let (?e68 (bvmul ?e67 ?e5))
84(let (?e69 (bvor ?e68 ?e4))
85(let (?e70 (bvmul ?e68 ?e6))
86(let (?e71 (bvmul ?e70 ?e69))
87(let (?e72 (bvor ?e71 ?e4))
88(let (?e73 (bvshl ?e72 (zero_extend[27] ?e62)))
89(let (?e74 (bvsub ?e62 ?e7))
90(let (?e75 (ite (bvuge ?e65 ?e73) bv1[1] bv0[1]))
91(let (?e76 (bvsub ?e65 ?e73))
92(let (?e77 (ite (= bv1[1] ?e75) ?e76 ?e65))
93(let (?e78 (bvor ?e68 ?e4))
94(let (?e79 (ite (= bv1[1] ?e75) ?e78 ?e68))
95(let (?e80 (bvmul ?e79 ?e5))
96(let (?e81 (bvor ?e80 ?e4))
97(let (?e82 (bvmul ?e80 ?e6))
98(let (?e83 (bvmul ?e82 ?e81))
99(let (?e84 (bvor ?e83 ?e4))
100(let (?e85 (bvshl ?e84 (zero_extend[27] ?e74)))
101(let (?e86 (bvsub ?e74 ?e7))
102(let (?e87 (ite (bvuge ?e77 ?e85) bv1[1] bv0[1]))
103(let (?e88 (bvsub ?e77 ?e85))
104(let (?e89 (ite (= bv1[1] ?e87) ?e88 ?e77))
105(let (?e90 (bvor ?e80 ?e4))
106(let (?e91 (ite (= bv1[1] ?e87) ?e90 ?e80))
107(let (?e92 (bvmul ?e91 ?e5))
108(let (?e93 (bvor ?e92 ?e4))
109(let (?e94 (bvmul ?e92 ?e6))
110(let (?e95 (bvmul ?e94 ?e93))
111(let (?e96 (bvor ?e95 ?e4))
112(let (?e97 (bvshl ?e96 (zero_extend[27] ?e86)))
113(let (?e98 (bvsub ?e86 ?e7))
114(let (?e99 (ite (bvuge ?e89 ?e97) bv1[1] bv0[1]))
115(let (?e100 (bvsub ?e89 ?e97))
116(let (?e101 (ite (= bv1[1] ?e99) ?e100 ?e89))
117(let (?e102 (bvor ?e92 ?e4))
118(let (?e103 (ite (= bv1[1] ?e99) ?e102 ?e92))
119(let (?e104 (bvmul ?e103 ?e5))
120(let (?e105 (bvor ?e104 ?e4))
121(let (?e106 (bvmul ?e104 ?e6))
122(let (?e107 (bvmul ?e106 ?e105))
123(let (?e108 (bvor ?e107 ?e4))
124(let (?e109 (bvshl ?e108 (zero_extend[27] ?e98)))
125(let (?e110 (bvsub ?e98 ?e7))
126(let (?e111 (ite (bvuge ?e101 ?e109) bv1[1] bv0[1]))
127(let (?e112 (bvsub ?e101 ?e109))
128(let (?e113 (ite (= bv1[1] ?e111) ?e112 ?e101))
129(let (?e114 (bvor ?e104 ?e4))
130(let (?e115 (ite (= bv1[1] ?e111) ?e114 ?e104))
131(let (?e116 (bvmul ?e115 ?e5))
132(let (?e117 (bvor ?e116 ?e4))
133(let (?e118 (bvmul ?e116 ?e6))
134(let (?e119 (bvmul ?e118 ?e117))
135(let (?e120 (bvor ?e119 ?e4))
136(let (?e121 (bvshl ?e120 (zero_extend[27] ?e110)))
137(let (?e122 (bvsub ?e110 ?e7))
138(let (?e123 (ite (bvuge ?e113 ?e121) bv1[1] bv0[1]))
139(let (?e124 (bvsub ?e113 ?e121))
140(let (?e125 (ite (= bv1[1] ?e123) ?e124 ?e113))
141(let (?e126 (bvor ?e116 ?e4))
142(let (?e127 (ite (= bv1[1] ?e123) ?e126 ?e116))
143(let (?e128 (bvmul ?e127 ?e5))
144(let (?e129 (bvor ?e128 ?e4))
145(let (?e130 (bvmul ?e128 ?e6))
146(let (?e131 (bvmul ?e130 ?e129))
147(let (?e132 (bvor ?e131 ?e4))
148(let (?e133 (bvshl ?e132 (zero_extend[27] ?e122)))
149(let (?e134 (bvsub ?e122 ?e7))
150(let (?e135 (ite (bvuge ?e125 ?e133) bv1[1] bv0[1]))
151(let (?e136 (bvsub ?e125 ?e133))
152(let (?e137 (ite (= bv1[1] ?e135) ?e136 ?e125))
153(let (?e138 (bvor ?e128 ?e4))
154(let (?e139 (ite (= bv1[1] ?e135) ?e138 ?e128))
155(let (?e140 (bvmul ?e139 ?e139))
156(let (?e141 (bvmul ?e140 ?e139))
157(let (?e142 (ite (= x ?e141) bv1[1] bv0[1]))
158(let (?e143 (bvadd ?e139 bv1[32]))
159(let (?e144 (bvmul ?e143 ?e143))
160(let (?e145 (bvmul ?e144 ?e143))
161(let (?e146 (ite (bvult ?e141 x) bv1[1] bv0[1]))
162(let (?e147 (ite (bvugt ?e145 x) bv1[1] bv0[1]))
163(let (?e148 (bvand ?e146 ?e147))
164(let (?e149 (bvor ?e142 ?e148))
165(not (= (bvnot ?e149) bv0[1]))
166)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
167