From d67fbf96a6053da3aaf171092ce4197e7e445477 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 27 Nov 2022 14:42:27 +0000 Subject: [PATCH] Better diagnostics on with_exprt and ifexprt type mismatch Makes it easier to understand which types are not matching. --- src/goto-symex/goto_symex_state.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 35f69067167..5414549d836 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -261,14 +261,15 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) *it = rename(std::move(*it), ns).get(); const exprt &c_expr = as_const(expr); - INVARIANT( + INVARIANT_WITH_DIAGNOSTICS( (expr.id() != ID_with || c_expr.type() == to_with_expr(c_expr).old().type()) && (expr.id() != ID_if || (c_expr.type() == to_if_expr(c_expr).true_case().type() && c_expr.type() == to_if_expr(c_expr).false_case().type())), "Type of renamed expr should be the same as operands for with_exprt and " - "if_exprt"); + "if_exprt", + irep_pretty_diagnosticst{expr}); if(level == L2) expr = field_sensitivity.apply(ns, *this, std::move(expr), false);