log/smt2perr146.smt2:1:18: expected ')' to close '(_ bv..' at '#x0'