Rename class to smt2_symbol_exprt

This reflects the inheritance from exprt and will avoid collision with
a type that will be introduced for smt2 ASTs.

Author: romainbrenguier

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -1751,7 +1751,7 @@ void java_string_library_preprocesst::initialize_conversion_table()
     ["java::java.lang.StringBuffer.append:(F)Ljava/lang/StringBuffer;"]=
       ID_cprover_string_concat_float_func;
   cprover_equivalent_to_java_assign_and_return_function
-    ["java::java.lang.StringBuffer.append:(I)Ljava/lang/StringBuffer;"]=
+    ["java::java.lang.StringBuffer.append:(I)Ljava/lang/StringBuffer;"] =
       ID_cprover_string_concat_int_func;
   cprover_equivalent_to_java_assign_and_return_function
     ["java::java.lang.StringBuffer.append:(J)Ljava/lang/StringBuffer;"]=

src/solvers/smt2/smt2_conv.cpp

@@ -1889,7 +1889,8 @@ void smt2_convt::convert_expr(const exprt &expr)
       // width must be multiple of bytes
       DATA_INVARIANT(
         width % bits_per_byte == 0,
-        "bit width indicated by type of bswap expression should be a multiple "
+        "bit width indicated by type of bswap expression should "
+        "be a multiple "
         "of the number of bits per byte");
 
       const std::size_t bytes = width / bits_per_byte;
@@ -4457,8 +4458,8 @@ void smt2_convt::find_symbols(const exprt &expr)
 
       exprt tmp1=expr;
       for(std::size_t i = 0; i < tmp1.operands().size(); i++)
-        tmp1.operands()[i]=
-          smt2_symbolt("op"+std::to_string(i), tmp1.operands()[i].type());
+        tmp1.operands()[i] = smt2_symbol_exprt(
+          "op" + std::to_string(i), tmp1.operands()[i].type());
 
       exprt tmp2=float_bv(tmp1);
       tmp2=letify(tmp2);

src/solvers/smt2/smt2_conv.h

@@ -154,10 +154,10 @@ class smt2_convt : public stack_decision_proceduret
   std::string floatbv_suffix(const exprt &) const;
   std::set<irep_idt> bvfp_set; // already converted
 
-  class smt2_symbolt : public nullary_exprt
+  class smt2_symbol_exprt : public nullary_exprt
   {
   public:
-    smt2_symbolt(const irep_idt &_identifier, const typet &_type)
+    smt2_symbol_exprt(const irep_idt &_identifier, const typet &_type)
       : nullary_exprt(ID_smt2_symbol, _type)
     { set(ID_identifier, _identifier); }
 
@@ -167,10 +167,10 @@ class smt2_convt : public stack_decision_proceduret
     }
   };
 
-  const smt2_symbolt &to_smt2_symbol(const exprt &expr)
+  const smt2_symbol_exprt &to_smt2_symbol(const exprt &expr)
   {
     assert(expr.id()==ID_smt2_symbol && !expr.has_operands());
-    return static_cast<const smt2_symbolt&>(expr);
+    return static_cast<const smt2_symbol_exprt &>(expr);
   }
 
   // flattens any non-bitvector type into a bitvector,