(assert (_ bv1 1 #x0