log/smt2perr110.smt2:1:10: first (high) 'extract' parameter 1 too large for bit-vector argument of bit-width 1