log/smt2perr042.smt2:2:1: expected 'BitVec' but reached end-of-file