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,12 @@ 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. old type:\n",
+    old_expr.type().pretty(),
+    "\nnew.type:\n",
+    new_expr.type().pretty());
   expr_map.insert(std::pair<irep_idt, exprt>(
     old_expr.get_identifier(), new_expr));
 }
@@ -46,7 +51,10 @@ 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. s.type:\n",
+    s.type().pretty(),
+    "\nit->second.type:\n",
+    it->second.type().pretty());
   static_cast<exprt &>(s) = it->second;
 
   return false;