Skip to content

Commit 050627f

Browse files
marek-trtiktautschnig
authored andcommitted
graphml: More precise detection of when to use '\result' variable.
1 parent afcbe92 commit 050627f

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

src/goto-programs/graphml_witness.cpp

+3-1
Original file line numberDiff line numberDiff line change
@@ -180,7 +180,9 @@ std::string graphml_witnesst::convert_assign_rec(
180180
exprt clean_lhs=assign.lhs();
181181
remove_l0_l1(clean_lhs);
182182
std::string lhs=expr_to_string(ns, identifier, clean_lhs);
183-
if(lhs.find('$')!=std::string::npos)
183+
if(lhs.find("#return_value")!=std::string::npos ||
184+
(lhs.find('$')!=std::string::npos &&
185+
lhs.find("return_value___VERIFIER_nondet_")==0U))
184186
lhs="\\result";
185187

186188
result=lhs+" = "+expr_to_string(ns, identifier, clean_rhs)+";";

0 commit comments

Comments
 (0)