log/smt2perr135.smt2:1:25: invalid 32-bit integer '10000000000'