(set-info :source "We verify the correctness of the ""next power of 2 algorithm""
from the book ""hacker's delight"" (Warren Jr., Henry).

Algorithm:
int next_power_of_2 (int x)
\\{
  int i;
  x-- >> nextpoweroftwo016.smt;
  for (i = 1; i < sizeof(int) * 8; i = i * 2)
  x = x | (x >> i)
  return x + 1;
\\}

Bit-width: 16

Contributed by Robert Brummayer (robert.brummayer@gmail.com).")
(set-info :status unsat)
(set-info :category "crafted")
(set-logic QF_BV)
(declare-fun x () (_ BitVec 16))
(assert (let ((_let_0 (bvadd x (bvadd (bvnot (_ bv1 16)) (_ bv1 16))))) (let ((_let_1 ((_ zero_extend 12) (_ bv1 4)))) (let ((_let_2 (bvnot _let_0))) (let ((_let_3 (bvand _let_2 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_0)) (bvnot (bvlshr _let_2 _let_1)) (bvlshr _let_0 _let_1)))))) (let ((_let_4 (bvnot _let_3))) (let ((_let_5 ((_ zero_extend 12) (_ bv2 4)))) (let ((_let_6 (bvand _let_3 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_4)) (bvnot (bvlshr _let_3 _let_5)) (bvlshr _let_4 _let_5)))))) (let ((_let_7 (bvnot _let_6))) (let ((_let_8 ((_ zero_extend 12) (_ bv3 4)))) (let ((_let_9 (bvand _let_6 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_7)) (bvnot (bvlshr _let_6 _let_8)) (bvlshr _let_7 _let_8)))))) (let ((_let_10 (bvnot _let_9))) (let ((_let_11 ((_ zero_extend 12) (_ bv4 4)))) (let ((_let_12 (bvand _let_9 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_10)) (bvnot (bvlshr _let_9 _let_11)) (bvlshr _let_10 _let_11)))))) (let ((_let_13 (bvnot _let_12))) (let ((_let_14 ((_ zero_extend 12) (_ bv5 4)))) (let ((_let_15 (bvand _let_12 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_13)) (bvnot (bvlshr _let_12 _let_14)) (bvlshr _let_13 _let_14)))))) (let ((_let_16 (bvnot _let_15))) (let ((_let_17 ((_ zero_extend 12) (_ bv6 4)))) (let ((_let_18 (bvand _let_15 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_16)) (bvnot (bvlshr _let_15 _let_17)) (bvlshr _let_16 _let_17)))))) (let ((_let_19 (bvnot _let_18))) (let ((_let_20 ((_ zero_extend 12) (_ bv7 4)))) (let ((_let_21 (bvand _let_18 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_19)) (bvnot (bvlshr _let_18 _let_20)) (bvlshr _let_19 _let_20)))))) (let ((_let_22 (bvnot _let_21))) (let ((_let_23 ((_ zero_extend 12) (_ bv8 4)))) (let ((_let_24 (bvand _let_21 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_22)) (bvnot (bvlshr _let_21 _let_23)) (bvlshr _let_22 _let_23)))))) (let ((_let_25 (bvnot _let_24))) (let ((_let_26 ((_ zero_extend 12) (_ bv9 4)))) (let ((_let_27 (bvand _let_24 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_25)) (bvnot (bvlshr _let_24 _let_26)) (bvlshr _let_25 _let_26)))))) (let ((_let_28 (bvnot _let_27))) (let ((_let_29 ((_ zero_extend 12) (_ bv10 4)))) (let ((_let_30 (bvand _let_27 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_28)) (bvnot (bvlshr _let_27 _let_29)) (bvlshr _let_28 _let_29)))))) (let ((_let_31 (bvnot _let_30))) (let ((_let_32 ((_ zero_extend 12) (_ bv11 4)))) (let ((_let_33 (bvand _let_30 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_31)) (bvnot (bvlshr _let_30 _let_32)) (bvlshr _let_31 _let_32)))))) (let ((_let_34 (bvnot _let_33))) (let ((_let_35 ((_ zero_extend 12) (_ bv12 4)))) (let ((_let_36 (bvand _let_33 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_34)) (bvnot (bvlshr _let_33 _let_35)) (bvlshr _let_34 _let_35)))))) (let ((_let_37 (bvnot _let_36))) (let ((_let_38 ((_ zero_extend 12) (_ bv13 4)))) (let ((_let_39 (bvand _let_36 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_37)) (bvnot (bvlshr _let_36 _let_38)) (bvlshr _let_37 _let_38)))))) (let ((_let_40 (bvnot _let_39))) (let ((_let_41 ((_ zero_extend 12) (_ bv14 4)))) (let ((_let_42 (bvand _let_39 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_40)) (bvnot (bvlshr _let_39 _let_41)) (bvlshr _let_40 _let_41)))))) (let ((_let_43 (bvnot _let_42))) (let ((_let_44 ((_ zero_extend 12) (_ bv15 4)))) (let ((_let_45 (bvlshr (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44)))))) _let_1))) (let ((_let_46 ((_ extract 15 15) _let_45))) (let ((_let_47 ((_ extract 15 15) x))) (let ((_let_48 (ite (bvult ((_ extract 14 0) _let_45) ((_ extract 14 0) x)) (_ bv1 1) (_ bv0 1)))) (let ((_let_49 (bvnot _let_47))) (let ((_let_50 ((_ extract 15 15) (_ bv1 16)))) (let ((_let_51 (ite (bvult ((_ extract 14 0) x) ((_ extract 14 0) (_ bv1 16))) (_ bv1 1) (_ bv0 1)))) (let ((_let_52 (bvnot _let_50))) (not (= (bvand (bvnot (bvand (bvand (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvnot (_ bv0 1)) (bvnot (ite (= (_ bv1 16) (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44))))))) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv2 16) (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44))))))) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv4 16) (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44))))))) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv8 16) (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44))))))) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv16 16) (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44))))))) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv32 16) (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44))))))) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv64 16) (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44))))))) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv128 16) (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44))))))) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv256 16) (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44))))))) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv512 16) (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44))))))) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv1024 16) (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44))))))) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv2048 16) (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44))))))) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv4096 16) (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44))))))) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv8192 16) (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44))))))) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv16384 16) (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44))))))) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= (_ bv32768 16) (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44))))))) (_ bv1 1) (_ bv0 1))))) (bvnot (ite (bvult (bvadd (_ bv1 16) (bvnot (bvand _let_42 (bvnot (ite (= (_ bv1 1) ((_ extract 15 15) _let_43)) (bvnot (bvlshr _let_42 _let_44)) (bvlshr _let_43 _let_44)))))) x) (_ bv1 1) (_ bv0 1)))) (bvnot (bvand (bvnot (bvand _let_46 _let_49)) (bvand (bvnot (bvand _let_48 (bvand (bvnot _let_46) _let_49))) (bvnot (bvand _let_48 (bvand _let_46 _let_47)))))))) (bvand (bvnot (bvand _let_47 _let_52)) (bvand (bvnot (bvand _let_51 (bvand _let_49 _let_52))) (bvnot (bvand _let_51 (bvand _let_47 _let_50)))))) (_ bv0 1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)