Merge pull request #7332 from tautschnig/feature/simp-diagnostics

kroening · web-flow · commit e5f607778ff3 · 2022-11-13T17:21:51.000Z
Simplifier type invariant: add diagnostic information
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
@@ -2975,7 +2975,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_rec(const exprt &expr)
   }
   else // change, new expression is 'tmp'
   {
-    POSTCONDITION(as_const(tmp).type() == expr.type());
+    POSTCONDITION_WITH_DIAGNOSTICS(
+      as_const(tmp).type() == expr.type(), tmp.pretty(), expr.pretty());
 
 #ifdef USE_CACHE
     // save in cache

Original file line number	Diff line number	Diff line change
`@@ -2975,7 +2975,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_rec(const exprt &expr)`
`2975`	`2975`	`}`
`2976`	`2976`	`else // change, new expression is 'tmp'`
`2977`	`2977`	`{`
`2978`		`- POSTCONDITION(as_const(tmp).type() == expr.type());`
	`2978`	`+ POSTCONDITION_WITH_DIAGNOSTICS(`
	`2979`	`+ as_const(tmp).type() == expr.type(), tmp.pretty(), expr.pretty());`
`2979`	`2980`
`2980`	`2981`	`#ifdef USE_CACHE`
`2981`	`2982`	`// save in cache`