From 1a22d3e2396d1064b9831387eca684e1e8815ecc Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 20 Apr 2023 10:49:39 +0000
Subject: [PATCH] Expr-to-C: output type information with nondet_symbol

This is a debugging aid to make the output of `--program-only` more
helpful when trying to see whether a call to malloc/calloc included type
information (via a sizeof annotation).
---
 src/ansi-c/expr2c.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 9472734f75b..9578d6d7376 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -1663,7 +1663,7 @@ std::string expr2ct::convert_symbol(const exprt &src)
 std::string expr2ct::convert_nondet_symbol(const nondet_symbol_exprt &src)
 {
   const irep_idt id=src.get_identifier();
-  return "nondet_symbol("+id2string(id)+")";
+  return "nondet_symbol<" + convert(src.type()) + ">(" + id2string(id) + ")";
 }
 
 std::string expr2ct::convert_predicate_symbol(const exprt &src)