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