(set-info :source "We write an arbitrary value into an array, assume that the array is sorted,
and finally verify that the binary search algorithm always finds this value.
Bit-width of elements: 32
Size of array: 16 elements

Contributed by Robert Brummayer (robert.brummayer@gmail.com).")
(set-info :status unsat)
(set-info :category "crafted")
(set-logic QF_AUFBV)
(declare-fun a17 () (Array (_ BitVec 4) (_ BitVec 32)))
(declare-fun search_val () (_ BitVec 32))
(declare-fun search_index () (_ BitVec 4))
(assert (let ((_let_0 (select (store a17 search_index search_val) (_ bv1 4)))) (let ((_let_1 (select (store a17 search_index search_val) (_ bv2 4)))) (let ((_let_2 (select (store a17 search_index search_val) (_ bv3 4)))) (let ((_let_3 (select (store a17 search_index search_val) (_ bv4 4)))) (let ((_let_4 (select (store a17 search_index search_val) (_ bv5 4)))) (let ((_let_5 (select (store a17 search_index search_val) (_ bv6 4)))) (let ((_let_6 (select (store a17 search_index search_val) (_ bv7 4)))) (let ((_let_7 (select (store a17 search_index search_val) (_ bv8 4)))) (let ((_let_8 (select (store a17 search_index search_val) (_ bv9 4)))) (let ((_let_9 (select (store a17 search_index search_val) (_ bv10 4)))) (let ((_let_10 (select (store a17 search_index search_val) (_ bv11 4)))) (let ((_let_11 (select (store a17 search_index search_val) (_ bv12 4)))) (let ((_let_12 (select (store a17 search_index search_val) (_ bv13 4)))) (let ((_let_13 (select (store a17 search_index search_val) (_ bv14 4)))) (let ((_let_14 (bvadd (_ bv0 4) (bvudiv (bvadd (_ bv15 4) (bvadd (bvnot (_ bv0 4)) (_ bv1 4))) (_ bv2 4))))) (let ((_let_15 (ite (= (_ bv1 1) (ite (bvult (select (store a17 search_index search_val) _let_14) search_val) (_ bv1 1) (_ bv0 1))) (bvadd (_ bv1 4) _let_14) (_ bv0 4)))) (let ((_let_16 (bvadd _let_15 (bvudiv (bvadd (ite (= (_ bv1 1) (ite (bvult search_val (select (store a17 search_index search_val) _let_14)) (_ bv1 1) (_ bv0 1))) (bvadd _let_14 (bvadd (bvnot (_ bv1 4)) (_ bv1 4))) (_ bv15 4)) (bvadd (_ bv1 4) (bvnot _let_15))) (_ bv2 4))))) (let ((_let_17 (ite (= (_ bv1 1) (ite (bvult (select (store a17 search_index search_val) _let_16) search_val) (_ bv1 1) (_ bv0 1))) (bvadd (_ bv1 4) _let_16) _let_15))) (let ((_let_18 (bvadd _let_17 (bvudiv (bvadd (ite (= (_ bv1 1) (ite (bvult search_val (select (store a17 search_index search_val) _let_16)) (_ bv1 1) (_ bv0 1))) (bvadd (bvadd (bvnot (_ bv1 4)) (_ bv1 4)) _let_16) (ite (= (_ bv1 1) (ite (bvult search_val (select (store a17 search_index search_val) _let_14)) (_ bv1 1) (_ bv0 1))) (bvadd _let_14 (bvadd (bvnot (_ bv1 4)) (_ bv1 4))) (_ bv15 4))) (bvadd (_ bv1 4) (bvnot _let_17))) (_ bv2 4))))) (let ((_let_19 (ite (= (_ bv1 1) (ite (bvult (select (store a17 search_index search_val) _let_18) search_val) (_ bv1 1) (_ bv0 1))) (bvadd (_ bv1 4) _let_18) _let_17))) (let ((_let_20 (bvadd _let_19 (bvudiv (bvadd (ite (= (_ bv1 1) (ite (bvult search_val (select (store a17 search_index search_val) _let_18)) (_ bv1 1) (_ bv0 1))) (bvadd (bvadd (bvnot (_ bv1 4)) (_ bv1 4)) _let_18) (ite (= (_ bv1 1) (ite (bvult search_val (select (store a17 search_index search_val) _let_16)) (_ bv1 1) (_ bv0 1))) (bvadd (bvadd (bvnot (_ bv1 4)) (_ bv1 4)) _let_16) (ite (= (_ bv1 1) (ite (bvult search_val (select (store a17 search_index search_val) _let_14)) (_ bv1 1) (_ bv0 1))) (bvadd _let_14 (bvadd (bvnot (_ bv1 4)) (_ bv1 4))) (_ bv15 4)))) (bvadd (_ bv1 4) (bvnot _let_19))) (_ bv2 4))))) (let ((_let_21 (select (store a17 search_index search_val) _let_20))) (let ((_let_22 (ite (= (_ bv1 1) (ite (bvult _let_21 search_val) (_ bv1 1) (_ bv0 1))) (bvadd (_ bv1 4) _let_20) _let_19))) (not (= (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (_ bv1 1) (bvnot (ite (bvult _let_0 (select (store a17 search_index search_val) (_ bv0 4))) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (bvult _let_1 _let_0) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (bvult _let_2 _let_1) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (bvult _let_3 _let_2) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (bvult _let_4 _let_3) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (bvult _let_5 _let_4) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (bvult _let_6 _let_5) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (bvult _let_7 _let_6) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (bvult _let_8 _let_7) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (bvult _let_9 _let_8) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (bvult _let_10 _let_9) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (bvult _let_11 _let_10) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (bvult _let_12 _let_11) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (bvult _let_13 _let_12) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (bvult (select (store a17 search_index search_val) (_ bv15 4)) _let_13) (_ bv1 1) (_ bv0 1)))) (bvand (bvand (bvand (bvand (bvand (bvnot (_ bv0 1)) (bvnot (ite (= search_val (select (store a17 search_index search_val) _let_14)) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= search_val (select (store a17 search_index search_val) _let_16)) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= search_val (select (store a17 search_index search_val) _let_18)) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= search_val _let_21) (_ bv1 1) (_ bv0 1)))) (bvnot (ite (= search_val (select (store a17 search_index search_val) (bvadd _let_22 (bvudiv (bvadd (ite (= (_ bv1 1) (ite (bvult search_val _let_21) (_ bv1 1) (_ bv0 1))) (bvadd (bvadd (bvnot (_ bv1 4)) (_ bv1 4)) _let_20) (ite (= (_ bv1 1) (ite (bvult search_val (select (store a17 search_index search_val) _let_18)) (_ bv1 1) (_ bv0 1))) (bvadd (bvadd (bvnot (_ bv1 4)) (_ bv1 4)) _let_18) (ite (= (_ bv1 1) (ite (bvult search_val (select (store a17 search_index search_val) _let_16)) (_ bv1 1) (_ bv0 1))) (bvadd (bvadd (bvnot (_ bv1 4)) (_ bv1 4)) _let_16) (ite (= (_ bv1 1) (ite (bvult search_val (select (store a17 search_index search_val) _let_14)) (_ bv1 1) (_ bv0 1))) (bvadd _let_14 (bvadd (bvnot (_ bv1 4)) (_ bv1 4))) (_ bv15 4))))) (bvadd (_ bv1 4) (bvnot _let_22))) (_ bv2 4))))) (_ bv1 1) (_ bv0 1))))) (_ bv0 1)))))))))))))))))))))))))))
(check-sat)