(declare-const a (_ BitVec 4294967296))