diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index ccae6ad7e55..2c382d76f98 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -278,24 +278,17 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) } if(it->type==goto_trace_stept::typet::ASSIGNMENT && - it->lhs_object_value.is_not_nil() && + it->full_lhs_value.is_not_nil() && it->full_lhs.is_not_nil()) { - if(!it->lhs_object_value.is_constant() || - !it->lhs_object_value.has_operands() || - !has_prefix(id2string(it->lhs_object_value.op0().get(ID_value)), - "INVALID-")) - { - xmlt &val=edge.new_element("data"); - val.set_attribute("key", "assumption"); - code_assignt assign(it->lhs_object, it->lhs_object_value); - irep_idt identifier=it->lhs_object.get_identifier(); - val.data=convert_assign_rec(identifier, assign); - - xmlt &val_s=edge.new_element("data"); - val_s.set_attribute("key", "assumption.scope"); - val_s.data=id2string(it->pc->source_location.get_function()); - } + xmlt &val=edge.new_element("data"); + val.set_attribute("key", "assumption"); + val.data=from_expr(ns, it->pc->function, it->full_lhs)+" = "+ + from_expr(ns, it->pc->function, it->full_lhs_value)+";"; + + xmlt &val_s=edge.new_element("data"); + val_s.set_attribute("key", "assumption.scope"); + val_s.data=id2string(it->pc->source_location.get_function()); } else if(it->type==goto_trace_stept::typet::GOTO && it->pc->is_goto())