(assert (_ bv0 2))