regress/parser/smt2perr172.smt2:2:21: expected bit-vector term of size 1 at index 0 as argument to 'fp'