Skip to content

Commit d7d9eb7

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

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

src/goto-programs/graphml_witness.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -165,7 +165,9 @@ std::string graphml_witnesst::convert_assign_rec(
165165
exprt clean_lhs=assign.lhs();
166166
remove_l0_l1(clean_lhs);
167167
std::string lhs=from_expr(ns, identifier, clean_lhs);
168-
if(lhs.find('$')!=std::string::npos)
168+
if(lhs.find("#return_value")!=std::string::npos ||
169+
(lhs.find('$')!=std::string::npos &&
170+
lhs.find("return_value___VERIFIER_nondet_")==0U))
169171
lhs="\\result";
170172

171173
result=lhs+" = "+from_expr(ns, identifier, clean_rhs)+";";

0 commit comments

Comments
 (0)