log/smt2perr155.smt2:2:1: expected decimal constant but reached end-of-file