graphml: More precise detection of when to use '\result' variable.

marek-trtik · Nov 27, 2017 · 9bdb376 · 9bdb376
1 parent 0d3c7fb
commit 9bdb376
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
@@ -161,7 +161,9 @@ std::string graphml_witnesst::convert_assign_rec(
     exprt clean_lhs=assign.lhs();
     remove_l0_l1(clean_lhs);
     std::string lhs=from_expr(ns, identifier, clean_lhs);
-    if(lhs.find('$')!=std::string::npos)
+    if(lhs.find("#return_value")!=std::string::npos ||
+       (lhs.find('$')!=std::string::npos &&
+        lhs.find("return_value___VERIFIER_nondet_")==0U))
       lhs="\\result";
 
     result=lhs+" = "+from_expr(ns, identifier, clean_rhs)+";";