Merge pull request #3652 from tautschnig/2064-simplifier-preserve-types

Make the simplifier preserve syntactically equal types [blocks: #2064]

Author: tautschnig

src/util/simplify_expr_int.cpp

@@ -955,7 +955,9 @@ bool simplify_exprt::simplify_concatenation(exprt &expr)
   }
 
   // { x } = x
-  if(expr.operands().size()==1)
+  if(
+    expr.operands().size() == 1 &&
+    base_type_eq(expr.op0().type(), expr.type(), ns))
   {
     exprt tmp;
     tmp.swap(expr.op0());

src/util/simplify_expr_struct.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include "arith_tools.h"
 #include "base_type.h"
 #include "byte_operators.h"
+#include "invariant.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
 #include "std_expr.h"
@@ -45,6 +46,9 @@ bool simplify_exprt::simplify_member(exprt &expr)
         if(op1.get(ID_component_name)==component_name)
         {
           // found it!
+          DATA_INVARIANT(
+            base_type_eq(op2.type(), expr.type(), ns),
+            "member expression type must match component type");
           exprt tmp;
           tmp.swap(op2);
           expr.swap(tmp);
@@ -134,6 +138,9 @@ bool simplify_exprt::simplify_member(exprt &expr)
       if(struct_type.has_component(component_name))
       {
         std::size_t number=struct_type.component_number(component_name);
+        DATA_INVARIANT(
+          base_type_eq(op.operands()[number].type(), expr.type(), ns),
+          "member expression type must match component type");
         exprt tmp;
         tmp.swap(op.operands()[number]);
         expr.swap(tmp);