Skip to content

Commit ad036c3

Browse files
tautschnigDaniel Kroening
authored and
Daniel Kroening
committed
Make sure SSA suffixes are stripped off GraphML output
Witness validators expect syntactically correct C code, and cannot cope with SSA suffixes.
1 parent 3af6711 commit ad036c3

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
@@ -141,7 +141,9 @@ std::string graphml_witnesst::convert_assign_rec(
141141
exprt clean_rhs=assign.rhs();
142142
remove_l0_l1(clean_rhs);
143143

144-
std::string lhs = expr_to_string(ns, identifier, assign.lhs());
144+
exprt clean_lhs = assign.lhs();
145+
remove_l0_l1(clean_lhs);
146+
std::string lhs = expr_to_string(ns, identifier, clean_lhs);
145147
if(lhs.find('$')!=std::string::npos)
146148
lhs="\\result";
147149

0 commit comments

Comments
 (0)