(declare-const a (_ BitVec 18446744073709551617))