@@ -280,14 +280,23 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
280280 expr.type () = to_with_expr (expr).old ().type ();
281281 }
282282 INVARIANT_WITH_DIAGNOSTICS (
283- (expr.id () != ID_with ||
284- c_expr.type () == to_with_expr (c_expr).old ().type ()) &&
285- (expr.id () != ID_if ||
286- (c_expr.type () == to_if_expr (c_expr).true_case ().type () &&
287- c_expr.type () == to_if_expr (c_expr).false_case ().type ())),
288- " Type of renamed expr should be the same as operands for with_exprt and "
289- " if_exprt" ,
290- irep_pretty_diagnosticst{expr});
283+ expr.id () != ID_with ||
284+ c_expr.type () == to_with_expr (c_expr).old ().type (),
285+ " Type of renamed expr should be the same as operands for with_exprt" ,
286+ c_expr.type ().pretty (),
287+ to_with_expr (c_expr).old ().type ().pretty ());
288+ INVARIANT_WITH_DIAGNOSTICS (
289+ expr.id () != ID_if ||
290+ c_expr.type () == to_if_expr (c_expr).true_case ().type (),
291+ " Type of renamed expr should be the same as operands for if_exprt" ,
292+ c_expr.type ().pretty (),
293+ to_if_expr (c_expr).true_case ().type ().pretty ());
294+ INVARIANT_WITH_DIAGNOSTICS (
295+ expr.id () != ID_if ||
296+ c_expr.type () == to_if_expr (c_expr).false_case ().type (),
297+ " Type of renamed expr should be the same as operands for if_exprt" ,
298+ c_expr.type ().pretty (),
299+ to_if_expr (c_expr).false_case ().type ().pretty ());
291300
292301 if (level == L2)
293302 expr = field_sensitivity.apply (ns, *this , std::move (expr), false );
0 commit comments