From 992b415df52ed8d25a3d3cf31e9d486ac20063d5 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 26 Sep 2018 08:48:59 +0000
Subject: [PATCH] Do not use deprecated symbol_exprt() in header file

std_expr.h is widely used, and using a deprecated constructor results in
spamming of log files.
---
 src/util/std_expr.h | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index d4f251222e8..5bc8883490c 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -4335,13 +4335,13 @@ class function_application_exprt:public binary_exprt
 public:
   function_application_exprt():binary_exprt(ID_function_application)
   {
-    op0()=symbol_exprt();
+    op0().id(ID_symbol);
   }
 
   explicit function_application_exprt(const typet &_type):
     binary_exprt(ID_function_application, _type)
   {
-    op0()=symbol_exprt();
+    op0().id(ID_symbol);
   }
 
   function_application_exprt(