regress/parser/smt2perr160.smt2:1:26: expected 64 bit integer