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( 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(s) = it->second; return false;