Skip to content

Commit 148fd45

Browse files
committed
ssa_exprt::get_object_name: add fast path
In many cases (without field sensitivity actually: always) the object will just be the original expression, no further processing is required. Thus add a fast path that handles this case directly, which reduces the cost from 967 seconds across all of SV-COMP's ReachSafety-ECA down to 143 seconds.
1 parent 7632d02 commit 148fd45

File tree

1 file changed

+6
-1
lines changed

1 file changed

+6
-1
lines changed

src/util/ssa_expr.h

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,8 +37,13 @@ class ssa_exprt:public symbol_exprt
3737

3838
irep_idt get_object_name() const
3939
{
40+
const exprt &original_expr = get_original_expr();
41+
42+
if(original_expr.id() == ID_symbol)
43+
return to_symbol_expr(original_expr).get_identifier();
44+
4045
object_descriptor_exprt ode;
41-
ode.object()=get_original_expr();
46+
ode.object() = original_expr;
4247
return to_symbol_expr(ode.root_object()).get_identifier();
4348
}
4449

0 commit comments

Comments
 (0)