simplify_concatenation is now independent of bitvector representation

This includes a fix to a bug where changes to the expression were not
signalled by returning 'false'.

Author: kroening

src/util/simplify_expr_int.cpp

@@ -887,8 +887,9 @@ bool simplify_exprt::simplify_concatenation(exprt &expr)
       exprt &op=*it;
       if(op.is_true() || op.is_false())
       {
-        bool value=op.is_true();
-        op=constant_exprt(value?ID_1:ID_0, unsignedbv_typet(1));
+        const bool value = op.is_true();
+        op = from_integer(value, unsignedbv_typet(1));
+        result = false;
       }
     }
 
@@ -906,13 +907,24 @@ bool simplify_exprt::simplify_concatenation(exprt &expr)
          is_bitvector_type(opn.type()))
       {
         // merge!
-        const std::string new_value=
-          opi.get_string(ID_value)+opn.get_string(ID_value);
-        opi.set(ID_value, new_value);
-        opi.type().set(ID_width, new_value.size());
+        const auto &value_i = to_constant_expr(opi).get_value();
+        const auto &value_n = to_constant_expr(opn).get_value();
+        const auto width_i = to_bitvector_type(opi.type()).get_width();
+        const auto width_n = to_bitvector_type(opn.type()).get_width();
+        const auto new_width = width_i + width_n;
+
+        const auto new_value = make_bvrep(
+          new_width, [&value_i, &value_n, width_i, width_n](std::size_t x) {
+            return x < width_n
+                     ? get_bitvector_bit(value_n, width_n, x)
+                     : get_bitvector_bit(value_i, width_i, x - width_n);
+          });
+
+        to_constant_expr(opi).set_value(new_value);
+        opi.type().set(ID_width, new_width);
         // erase opn
         expr.operands().erase(expr.operands().begin()+i+1);
-        result=true;
+        result = false;
       }
       else
         i++;
@@ -943,7 +955,7 @@ bool simplify_exprt::simplify_concatenation(exprt &expr)
         opi.type().id(ID_verilog_unsignedbv);
         // erase opn
         expr.operands().erase(expr.operands().begin()+i+1);
-        result=true;
+        result = false;
       }
       else
         i++;