Use plus_exprt constructor that does not take a type

The type of the plus_exprt is the type of the lhs by default. This is
always the case in the code base.

Author: antlechner

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2858,7 +2858,7 @@ exprt java_bytecode_convert_methodt::convert_aload(
   const member_exprt data_ptr(
     deref, "data", pointer_type(java_type_from_char(type_char)));
 
-  plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type());
+  plus_exprt data_plus_offset{data_ptr, op[1]};
   // tag it so it's easy to identify during instrumentation
   data_plus_offset.set(ID_java_array_access, true);
   const dereference_exprt element{data_plus_offset};
@@ -2906,7 +2906,7 @@ code_blockt java_bytecode_convert_methodt::convert_astore(
   const member_exprt data_ptr(
     deref, "data", pointer_type(java_type_from_char(type_char)));
 
-  plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type());
+  plus_exprt data_plus_offset{data_ptr, op[1]};
   // tag it so it's easy to identify during instrumentation
   data_plus_offset.set(ID_java_array_access, true);
   const dereference_exprt element{data_plus_offset};

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1217,7 +1217,7 @@ void java_object_factoryt::array_loop_init_code(
   }
 
   const dereference_exprt arraycellref{
-    plus_exprt{array_init_symexpr, counter_expr, array_init_symexpr.type()}};
+    plus_exprt{array_init_symexpr, counter_expr}};
 
   // MUST_UPDATE_IN_PLACE only applies to this object.
   // If this is a pointer to another object, offer the chance

src/analyses/goto_check.cpp

@@ -1108,7 +1108,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
 
       binary_relation_exprt lb_check(a.first, ID_le, int_ptr);
 
-      plus_exprt ub(int_ptr, size, int_ptr.type());
+      plus_exprt ub{int_ptr, size};
 
       binary_relation_exprt ub_check(ub, ID_le, plus_exprt(a.first, a.second));
 

src/solvers/smt2/smt2_conv.cpp

@@ -561,10 +561,7 @@ void smt2_convt::convert_address_of_rec(
         new_index_expr,
         pointer_type(array.type().subtype()));
 
-      plus_exprt plus_expr(
-        address_of_expr,
-        index,
-        address_of_expr.type());
+      plus_exprt plus_expr{address_of_expr, index};
 
       convert_expr(plus_expr);
     }