SMT2 backend: use FPA theory with --cprover-smt2

This enables the use of the FloatingPoint theory when using cprover_smt2.
The resulting SMT-LIB files are much smaller, and easier to read.

The commit also enables existing tests that now pass with --cprover-smt2.

Author: kroening

regression/cbmc/Float-div2/test.desc

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

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

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

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

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

regression/cbmc/Float20/test.desc

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

regression/cbmc/Float23/test.desc

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

regression/cbmc/Float3/test.desc

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

regression/cbmc/Float5/test.desc

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

regression/cbmc/Float6/test.desc

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

regression/cbmc/Float8/test.desc

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

src/solvers/smt2/smt2_conv.cpp

@@ -85,6 +85,7 @@ smt2_convt::smt2_convt(
     break;
 
   case solvert::CPROVER_SMT2:
+    use_FPA_theory = true;
     use_array_of_bool = true;
     use_as_const = true;
     use_check_sat_assuming = true;