Merge pull request #7390 from peterschrammel/ifexprt-diagnostics

Better diagnostics on with_exprt and ifexprt type mismatch

Author: tautschnig

src/goto-symex/goto_symex_state.cpp

@@ -261,14 +261,15 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
       *it = rename<level>(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);