Improve replace_symbolt precondition message

Invariant violations now print out the actual types that were
mismatched.

Author: karkhaz

src/util/replace_symbol.cpp

@@ -25,7 +25,11 @@ void replace_symbolt::insert(
   const symbol_exprt &old_expr,
   const exprt &new_expr)
 {
-  PRECONDITION(old_expr.type() == new_expr.type());
+  PRECONDITION_WITH_DIAGNOSTICS(
+    old_expr.type() == new_expr.type(),
+    "types to be replaced should match.\nold type: '" +
+      old_expr.type().pretty() + "'\nnew.type: '" + new_expr.type().pretty() +
+      "')");
   expr_map.insert(std::pair<irep_idt, exprt>(
     old_expr.get_identifier(), new_expr));
 }
@@ -46,7 +50,8 @@ bool replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
 
   DATA_INVARIANT(
     s.type() == it->second.type(),
-    "type of symbol to be replaced should match");
+    "types to be replaced should match.\ns.type: '" + s.type().pretty() +
+      "'\nit->second.type: '" + it->second.type().pretty() + "')");
   static_cast<exprt &>(s) = it->second;
 
   return false;