Correct pretty-printing of code_returnt

diffblue · Mar 23, 2017 · e843b72 · e843b72
1 parent a7663cb
commit e843b72
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -3337,7 +3337,7 @@ std::string expr2ct::convert_code_return(
   std::string dest=indent_str(indent);
   dest+="return";
 
-  if(src.operands().size()==1)
+  if(to_code_return(src).has_return_value())
     dest+=" "+convert(src.op0());
 
   dest+=';';