(assert (= (_ bv0 2) (_ bv1 2) (_ bv1 1)))