regress/parser/smt2perr144.smt2:1:16: expected 64 bit integer