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