log/smt2perr165.smt2:1:28: invalid 32-bit integer '4294967296'