log/smt2perr050.smt2:3:1: expected ')' to close bit-vector sort at end-of-file