regress/parser/smt2perr159.smt2:1:24: expected 64 bit integer