From 52001fa838fbe517a62ff0cc9b6a8c22ed03939c Mon Sep 17 00:00:00 2001
From: Kareem Khazem <karkhaz@amazon.com>
Date: Wed, 29 Jan 2020 17:40:38 +0000
Subject: [PATCH] Improve replace_symbolt precondition message

Invariant violations now print out the actual types that were
mismatched.
---
 src/util/replace_symbol.cpp | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp
index b1aae718b8c..c7844708e1c 100644
--- a/src/util/replace_symbol.cpp
+++ b/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;