log/smt2perr156.smt2:1:8: expected expression