boolbv: fix fixedbv-type check in convert_rest for ID_isfinite

The ID_isfinite branch in boolbvt::convert_rest tested
'op.id() == ID_fixedbv', but ID_fixedbv is a *type* id and op is the
operand expression, not a type.  The dead branch never matched and
fixedbv operands fell through to SUB::convert_rest, which is not
prepared to lower an isfinite expression and would yield an
unexpected result or conversion failure.

The neighbouring ID_isnan, ID_isinf, and ID_isnormal branches all
correctly use 'op.type().id() == ID_fixedbv'.  Bring ID_isfinite
into line.

Pre-existing typo, unrelated to the surrounding refactoring; fixed
here because it sits in the immediate neighbourhood of changes to
the floatbv branch and to keep the fixedbv handling consistent.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

src/solvers/flattening/boolbv.cpp

@@ -461,7 +461,7 @@ literalt boolbvt::convert_rest(const exprt &expr)
         !float_utils.is_infinity(bv),
         !float_utils.is_NaN(bv));
     }
-    else if(op.id() == ID_fixedbv)
+    else if(op.type().id() == ID_fixedbv)
       return const_literal(true);
   }
   else if(expr.id()==ID_isinf)