log/smt2perr121.smt2:3:1: expected symbol to be bound after '(' at line 1 column 15 but reached end-of-file