(declare-fun a ()