(declare-fun a((_ BitVec 0.1