SMT2 back-end and solver: it's fp.isInfinite, not fp.isInf

We already had gotten this right in one place, but got in wrong in 5
other places.

Fixes: #1782

Author: tautschnig

regression/cbmc/Float8/smt.desc

@@ -0,0 +1,8 @@
+CORE smt-backend
+main.c
+--smt2 --fpa
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/solvers/smt2/smt2_conv.cpp

@@ -1859,7 +1859,7 @@ void smt2_convt::convert_expr(const exprt &expr)
         convert_expr(isfinite_expr.op());
         out << "))";
 
-        out << "(not (fp.isInf ";
+        out << "(not (fp.isInfinite ";
         convert_expr(isfinite_expr.op());
         out << "))";
 

src/solvers/smt2/smt2_parser.cpp

@@ -1245,14 +1245,14 @@ void smt2_parsert::setup_expressions()
     return unary_predicate_exprt(ID_isnan, op[0]);
   };
 
-  expressions["fp.isInf"] = [this] {
+  expressions["fp.isInfinite"] = [this] {
     auto op = operands();
 
     if(op.size() != 1)
-      throw error("fp.isInf takes one operand");
+      throw error("fp.isInfinite takes one operand");
 
     if(op[0].type().id() != ID_floatbv)
-      throw error("fp.isInf takes FloatingPoint operand");
+      throw error("fp.isInfinite takes FloatingPoint operand");
 
     return unary_predicate_exprt(ID_isinf, op[0]);
   };