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,10 @@ 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 +49,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. s.type:\n" + s.type().pretty() +
+      "\nit->second.type:\n" + it->second.type().pretty());
   static_cast<exprt &>(s) = it->second;
 
   return false;