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