regress/parser/smt2perr049.smt2:1:36: expected 64 bit integer