diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index c1e77a3c5f1..8f27a3c0e02 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -455,7 +455,7 @@ class goto_symext
   virtual void symex_fkt(statet &, const code_function_callt &);
   virtual void symex_macro(statet &, const code_function_callt &);
   virtual void symex_trace(statet &, const code_function_callt &);
-  virtual void symex_printf(statet &, const exprt &lhs, const exprt &rhs);
+  virtual void symex_printf(statet &, const exprt &rhs);
   virtual void symex_input(statet &, const codet &);
   virtual void symex_output(statet &, const codet &);
 
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index d9dcc19c498..ce5d7ee0775 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -54,7 +54,11 @@ void goto_symext::symex_assign(
     else if(statement==ID_allocate)
       symex_allocate(state, lhs, side_effect_expr);
     else if(statement==ID_printf)
-      symex_printf(state, lhs, side_effect_expr);
+    {
+      if(lhs.is_not_nil())
+        throw "printf: unexpected assignment";
+      symex_printf(state, side_effect_expr);
+    }
     else if(statement==ID_gcc_builtin_va_arg_next)
       symex_gcc_builtin_va_arg_next(state, lhs, side_effect_expr);
     else
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 0d6455dc142..7b4be956854 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -311,7 +311,6 @@ irep_idt get_string_argument(const exprt &src, const namespacet &ns)
 
 void goto_symext::symex_printf(
   statet &state,
-  const exprt &lhs,
   const exprt &rhs)
 {
   if(rhs.operands().empty())
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index 30ca539f429..c1ceff5c12d 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -101,7 +101,7 @@ void goto_symext::symex_other(
   {
     codet clean_code=code;
     clean_expr(clean_code, state, false);
-    symex_printf(state, nil_exprt(), clean_code);
+    symex_printf(state, clean_code);
   }
   else if(statement==ID_input)
   {