log/smt2perr043.smt2:1:29: expected 'BitVec' at 'BitVector'