regress/parser/smt2perr140.smt2:1:21: expected 64 bit integer