(declare-fun a () |no symbol allowed here|