diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h index 5454f07c5ba..59120684d52 100644 --- a/src/util/ssa_expr.h +++ b/src/util/ssa_expr.h @@ -37,8 +37,13 @@ class ssa_exprt:public symbol_exprt irep_idt get_object_name() const { + const exprt &original_expr = get_original_expr(); + + if(original_expr.id() == ID_symbol) + return to_symbol_expr(original_expr).get_identifier(); + object_descriptor_exprt ode; - ode.object()=get_original_expr(); + ode.object() = original_expr; return to_symbol_expr(ode.root_object()).get_identifier(); }