log/smt2perr122.smt2:2:3: expected symbol to be bound at '#x12' after '(' at line 1 column 15