log/smt2perr159.smt2:1:24: invalid 32-bit integer '8.0'