Merge pull request #6960 from tautschnig/bugfixes/1782-smt2-isinfinite

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

Author: tautschnig

regression/cbmc/Float-no-simp4/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --floatbv --no-simplify
 ^EXIT=0$

regression/cbmc/Float4/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --floatbv
 ^EXIT=0$

regression/cbmc/Float8/smt.desc

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

regression/cbmc/pragma_cprover_enable_all/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --object-bits 8 --bounds-check --pointer-check --pointer-primitive-check --div-by-zero-check --enum-range-check --unsigned-overflow-check --signed-overflow-check --pointer-overflow-check --float-overflow-check --conversion-check --undefined-shift-check --nan-check --pointer-primitive-check
 ^\[main\.pointer_primitives\.\d+\] line 77 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$

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]);
   };