log/smt2perr080.smt2:3:10: first argument of '=' is an array with index bit-vectors of width 64 but argument 2 is an array with index bit-vectors of width 32