regress/parser/smt2perr110.smt2:1:21: upper index '1' too high for bit-vector of size 1 as argument to 'extract'