From e843b724ec4c155e576a6551b24c0dc6e41c865e Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 20 Mar 2017 16:09:49 +0000 Subject: [PATCH] Correct pretty-printing of code_returnt --- 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 a6975bdab19..86bd4183b91 100644 --- 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+=';';