Skip to content

Commit 4a3fa35

Browse files
committed
Don't simplify guard to skip instructions
Which is cheaper: simplifying a large guard, or checking that goto_state_map doesn't contain any incoming entries for the instructions between this one and the jump target? My theory: the latter.
1 parent fe75b71 commit 4a3fa35

File tree

1 file changed

+4
-6
lines changed

1 file changed

+4
-6
lines changed

src/goto-symex/symex_goto.cpp

+4-6
Original file line numberDiff line numberDiff line change
@@ -106,15 +106,13 @@ void goto_symext::symex_goto(statet &state)
106106
}
107107
}
108108

109-
exprt simpl_state_guard = state.guard.as_expr();
110-
do_simplify(simpl_state_guard);
111-
112109
// No point executing both branches of an unconditional goto.
113110
if(
114111
new_guard.is_true() && // We have an unconditional goto, AND
115-
// either there are no blocks between us and the target in the
116-
// surrounding scope
117-
(simpl_state_guard.is_true() ||
112+
// either there are no reachable blocks between us and the target in the
113+
// surrounding scope (because state.guard == true implies there is no path
114+
// around this GOTO instruction)
115+
(state.guard.is_true() ||
118116
// or there is another block, but we're doing path exploration so
119117
// we're going to skip over it for now and return to it later.
120118
symex_config.doing_path_exploration))

0 commit comments

Comments
 (0)