Skip to content

Commit f81c8c0

Browse files
authored
Merge pull request #6435 from diffblue/goto_program_return_output2
output "SET RETURN VALUE" when displaying goto programs
2 parents ce3fcaa + c65874f commit f81c8c0

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/goto-programs/goto_program.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -133,7 +133,7 @@ std::ostream &goto_programt::output_instruction(
133133
break;
134134

135135
case SET_RETURN_VALUE:
136-
out << "RETURN " << format(instruction.return_value()) << '\n';
136+
out << "SET RETURN VALUE " << format(instruction.return_value()) << '\n';
137137
break;
138138

139139
case DECL:

0 commit comments

Comments
 (0)