(assert (ite (_ bv1 1) (_ bv0 16) (_ bv0 15))