regress/parser/smt2perr141.smt2:1:22: expected 64 bit integer