(declare-fun "a string is not a symbol")