regress/parser/smt2perr163.smt2:2:28: expected bit-vector term at index 1 as argument to 'concat'